Mechanizing Matching Logic In Coq

Péter Bereczky
(Eötvös Loránd University, Hungary)
Xiaohong Chen
(University of Illinois at Urbana-Champaign, USA)
Dániel Horpácsi
(Eötvös Loránd University, Hungary)
Lucas Peña
(University of Illinois at Urbana-Champaign, USA)
Jan Tušil
(Masaryk University, Czechia)

Matching logic is a formalism for specifying, and reasoning about, mathematical structures, using patterns and pattern matching. Growing in popularity, it has been used to define many logical systems such as separation logic with recursive definitions and linear temporal logic. In addition, it serves as the logical foundation of the K semantic framework, which was used to build practical verifiers for a number of real-world languages. Despite being a fundamental formal system accommodating substantial theories, matching logic lacks a general-purpose, machine-checked formalization. Hence, we formalize matching logic using the Coq proof assistant. Specifically, we create a new representation of matching logic that uses a locally nameless encoding, and we formalize the syntax, semantics, and proof system of this representation in the Coq proof assistant. Crucially, we prove the soundness of the formalized proof system and provide a means to carry out interactive matching logic reasoning in Coq. We believe this work provides a previously unexplored avenue for reasoning about matching logic, its models, and the proof system.

In Vlad Rusu: Proceedings of the Sixth Working Formal Methods Symposium (FROM 2022), "Al. I. Cuza University", Iasi, Romania, 19-20 September, 2022, Electronic Proceedings in Theoretical Computer Science 369, pp. 17–36.
Published: 19th September 2022.

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