An Interactive Theorem Prover for Matching Logic with Proof Object Generation

Matching logic is a uniform logical foundation for K, which is a language semantics framework with the philosophy that all tooling around a language should be automatically generated from a single, rigorous definition of its formal semantics. In practice, K has been widely used to define the formal semantics of many real-world languages and to generate their execution and verification tools. However, there lacks a generic theorem prover that connects K with its logical foundation—matching logic. In this paper, we present ITPML, which is the first interactive theorem prover for matching logic. The main advantage of ITPML is its ability to generate machine-checkable proof objects as certificates that witness the correctness of its formal reasoning. ITPML is built on top of Metamath, a language to define formal systems, which allows it to have a small trust base of only 250 lines of code. ITPML supports both backward and forward proofs, allows users to dynamically add intermediate lemmas, and features automated proof tactics for common utilities such as reasoning about notations and proving propositional tautologies.