On October 19, 2023 at 14:00 EEST, Horațiu Cheval (University of Bucharest) will give a talk in the Logic Seminar.
Title: Matching Logic in Lean
Abstract:
Matching Logic is a small and expressive system aimed at program verification, constituting the theoretical underpinning of the 𝕂 framework. We present a Lean formalization of the applicative version of Matching Logic (AML), with definitions for the proof system and semantics, together with proofs of some metatheoretical results, like the deduction and soundness theorems. We also present a work-in-progress mechanism for automatically translating AML proofs from our Lean formalization to an existing encoding of AML in the Metamath proof checker. Two different methods are presented, one at the object level, and one based on metaprogramming. The implementations are available here and here.
The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.