Mechanizing Matching Logic In Coq

TL;DR

This paper formalizes matching logic within Coq, providing a sound proof system and enabling interactive reasoning, which was previously lacking for this foundational formalism used in various logical systems.

Contribution

It introduces a Coq formalization of matching logic with a locally nameless encoding, including syntax, semantics, and proof system, and proves its soundness.

Findings

Formalization of matching logic in Coq using locally nameless encoding

Proof of soundness for the formalized proof system

Enables interactive reasoning about matching logic in Coq

Abstract

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.