A Gentle Introduction to Matching Logic and its Applications

Mar 29 14:00 ₂₀₂₃

Abstract: Matching Logic (ML) allows to uniformly specify and reason about programming languages and properties of their programs. It was developed as a logical foundation of the K framework.

ML is expressive enough to specify all properties within various logical systems such as FOL, separation logic,  lambda-calculus, (dependent) type systems, and modal  mu-calculus. In particular, it supports operational semantics (term rewriting) and axiomatic semantics (Hoare triples). ML has a sound  fixed Hilbert-style proof system that supports formal reasoning for all specifications. In this talk we give a gentle introduction to (Applicative) Matching Logic [3], we show how the initial algebraic semantics can be encoded as ML theories [4], and how ML is used to formaly define programming languages semantics and program properties.

References:

1. Grigore Rosu. Matching Logic, LMCS, 2017.
2. Xiaohong Chen and Grigore Roşu.Matching 𝜇-logic. LICS 2019.
3. Xiaohong Chen, Dorel Lucanu, Grigore Rosu: Matching logic explained. JLAMP 2021
4. Xiaohong Chen and Dorel Lucanu and Grigore Rosu. Initial algebra semantics in matching logic.Technical Report July 2020
5. Xiaohong Chen and Grigore Rosu. Matching mu-Logic: Foundation of K Framework, CALCO'19

Short biography: Dorel Lucanu is a full professor at the Faculty of Computer Science, Alexandru Ioan Cuza University of Iași, Romania, where he founded and is leading the Formal Methods in Software Engineering research group. His research interests lie within the area of formal methods applied in software engineering, with a focus on logic for programs (rewriting logic, matching logic), (circular) coinductive reasoning, program verification, and program analysis (including malware analysis). Dorel Lucanu is also a collaborator of Runtimev Verification RV, a startup that develops the current version of the K Framework.