Unification in Matching Logic — Revisited

Ádám Kurucz
(ELTE Eötvös Loránd University)
Péter Bereczky
(ELTE Eötvös Loránd University)
Dániel Horpácsi
(ELTE Eötvös Loránd University)

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.

In Mircea Marin and Laurenţiu Leuştean: Proceedings Eighth Symposium on Working Formal Methods (FROM 2024), Timişoara, Romania, September 16-18, Electronic Proceedings in Theoretical Computer Science 410, pp. 1–17.
Published: 31st October 2024.

ArXived at: https://dx.doi.org/10.4204/EPTCS.410.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org