Unification in Matching Logic -- Revisited

TL;DR

This paper revisits the unification problem in matching logic, extending previous algorithms to an applicative variant and mechanizing the solution in Coq for improved reasoning about program specifications.

Contribution

It generalizes the unification algorithm to the applicative variant of matching logic and formalizes the solution in Coq, enhancing its applicability and correctness.

Findings

Generalized unification algorithm for applicative matching logic

Mechanized proof of correctness in Coq

Improved practical reasoning about program patterns

Abstract

Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern 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. This is easily remedied by unification, for which an algorithm has 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 generalising the unification problem and mechanizing a proven-sound solution in Coq.