July 2022 – March 2023
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
- Bogdan Macovei
ILDS Management Team:
Description:
Matching logic (ML), developed by Grigore Roşu and his collaborators, is a unifying logic for defining formal semantics of programming languages and for specifying and reasoning about the behavior of programs. Lean is a functional programming language that can also be used as an interactive theorem prover.
The main goal of this project is to enhance the ML ecosystem by adding Lean support.
Our first objective is to formalize ML in Lean. This will be similar in principle to and will be inspired from the recent formalization of ML in Coq, but it will be optimized and specialized to Lean, taking advantage of its strengths.
The second objective is to generate proof objects in Metamath, a computer language for mathematical proofs that is simple, fast, and trustworthy. This will be obtained by combining the Lean formalization of ML and the Metamath proof checker for ML. In this way we shall increase the confidence in the correctness of the ML proofs and proof checking will be much more efficient, as it will be done by a very small proof checker. More…
Results:
- L. Leuștean, Notes on Applicative Matching Logic, October 2022.
- H. Cheval, B. Macovei, Lean formalization of Applicative Matching Logic.
- H. Cheval, Extracting Matching Logic proofs from Lean to Metamath.