April 2023 – December 2025
Research Partners:
- Runtime Verification
- Research Center for Logic, Optimization & Security (LOS), University of Bucharest
Research Team:
- Laurenţiu Leuştean (Principal Investigator)
- Horaţiu Cheval
- Alexandru Oltean
- Dafina Trufaș
ILDS Management Team:
Description:
As part of the previous RV/ILDS project, we have formalized and implemented a deep embedding of Applicative Matching Logic (AML) into the Lean prover with the ability to perform proofs in AML and export Metamath proof objects which are checkable by the Metamath formalization of AML.
The next natural step towards realizing a connection to 𝕂 is to build on this foundation the formalization of Matching μ-Logic (μML), whose textual representation is KORE, the current intermediate representation for the 𝕂 language. For this, we propose the following objectives.
The first objective is a theoretical one and consists of defining an embedding of μML into AML, both at the syntactical level and at the semantical level. We shall take the following steps: translate μML signatures into AML specifications; translate μML specifications into AML specifications; translate AML models corresponding to translations of μML signatures into μML models; show that the syntactic and semantic translations form an embedding of μML into AML (e.g., by using a comorphism of institutions).
The second objective concerns the Lean formalization of this translation. We shall formalize in Lean the following: the syntax and proof system of μML; proofs of μML theorems and derived deduction rules; a proof of the deduction theorem; examples of theories with proofs about their properties; the syntactic translations defined in the first objective; proofs of μML deduction rules as theorems in the corresponding embedding into AML.
The third objective concerns the implementation of a way to translate KORE specification (as generated by the 𝕂 front-end) into Lean μML specifications (as formalized in the first two objectives). This will form the final link in a KORE-μML-AML-Metamath tool-chain. To illustrate this, we will import the specification of a small language from 𝕂 into Lean, we will manually certify an execution using the μML proof system, we will export the proof object into Metamath and, finally, we will check its correctness against the Metamath specification of AML.