Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern in normal form is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. The number of structural components can be reduced by unification and anti-unification. Algorithms for both processes have already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language, while generalizing the unification problem and mechanizing a proven-sound solution in Coq, as well as exploring certain possible extensions of the unification algorithm in a semi-formalized manner.

Matching logic is a general formal framework for reasoning about a wide range of theories, with particular emphasis on programming language semantics. Semantic reasoning, such as proof of satisfaction, requires the logic to be expressed within a foundational theory; adopting a dependently typed setting enables well-sortedness in the object theory to correspond directly to well-typedness in the host theory. In this paper, we present the first dependently typed, locally nameless definition of matching μ -logic, including both syntax and semantics, ensuring well-sortedness and local closedness via sorted contexts encoded in type indices. As a result, ill-sorted syntax is unrepresentable, and the semantics of well-sorted elements are guaranteed to lie within the domains of their associated sorts. We also demonstrate how this encoding facilitates model-theoretic reasoning about the consistency of matching logic theories.

We aim to reason about the correctness of behaviour-preserving transformations of Erlang programs. Behaviour preservation is characterised by semantic equivalence. Based upon our existing formal semantics for Core Erlang, we investigate potential definitions of suitable equivalence relations. In particular we adapt a number of existing approaches of expression equivalence to a simple functional programming language that carries the main features of sequential Core Erlang; we then examine the properties of the equivalence relations and formally establish connections between them. The results presented in this paper, including all theorems and their proofs, have been machine checked using the Coq proof assistant.