Proof-carrying parameters in certified symbolic execution.

This article focuses on generating proof objects for unification and antiunification algorithms within the framework of matching logic (Ml), a logical system used to formally define programming languages and reason about program executions. It presents formalizations of syntactic unification and Plotkin's antiunification algorithms as transformations of Ml patterns, proving their soundness and completeness relative to the Ml theory of many-sorted term algebras. The authors develop a generic method to generate proof objects—structured formal proofs certifying equivalences between original and normalized patterns—by instrumenting each algorithmic step, and instantiate this method specifically for unification and antiunification. A prototype implementation in Maude demonstrates the feasibility of automatically generating and checking these proof objects on complex inputs inspired by real-world language definitions (e.g., C and Java in the K framework), showing that proof object sizes scale linearly with algorithm steps. The work aims to enhance trustworthiness in tools derived from formal language definitions by providing externally checkable correctness certificates for symbolic execution steps involving (anti)unification.