On November 9, 2023 at 14:00 EET, Traian Șerbănuță (University of Bucharest/Runtime Verification/ILDS) will give a talk in the Logic Seminar.
Title: Yet another formalization of matching logic in Coq
Abstract:
This talk will describe an exercise in formalizing and verifying, with the help of the proof assistant Coq, Laurențiu Leuștean’s notes on matching logic [1], including the syntax, the proof system, models, satisfaction, and soundness, as well as some elements of set theory (including Tarski and Kleene’s fixed point theorems as specialized for sets).
References:
[1] L. Leuștean, Notes on applicative matching logic, 2022.
The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.