Thursday 20 February 2020, 14:00, LSV library: Matching Logic: Theory and Proofs, Dorel Lucanu (Alexandru Ioan Cuza University), joint work with Traian Serbanuta, Xiaohong Chen and Grigore Rosu.

Matching logic is a unifying foundational logic for programming languages, specification and verification. It serves as the foundation of the K framework: a formal language framework where all programming languages must have a formal semantics and all language tools are automatically generated by the framework from the semantics at no additional costs, in a correct-by-construction manner. Matching logic allows us to regard a programming language through both operational and axiomatic lenses at the same time, making no distinction between the two. The semantics of a programming language is given in matching logic as a set of particular formulas (patterns) that formalize logically constrained rewrite rules. Both operational behaviors and formal properties of a program are derived using the language-independent proof system of matching logic: the same proof system to reason about all programming languages. From the logical point of view, matching logic is a powerful extension of the normal modal logic with many-sorted universes, many-sorted modalities, first-order logic (FOL) quantifiers ∀ and ∃, and the least fixpoint μ-binder. Many logics/calculi/models, especially those important in the study of programming languages, can be defined as theories in matching logic. In this talk we give a gentle introduction in matching logic and a brief presentation of two matching-logic-based tools (provers).

References:
[Chen&Rosu 2019a] Xiaohong Chen and Grigore Rosu. Applicative Matching Logic.
Technical Report http://hdl.handle.net/2142/104616, July 2019 [Chen&Rosu 2019b] Xiaohong Chen and Grigore Rosu. Matching mu-Logic: Foundation of K Framework, CALCO'19, Leibniz International Proceedings in Informatics (LIPIcs) 139, pp 1-4. 2019
[Rosu 2017] Grigore Roşu. Matching logic. Logical Methods in Computer Science, 13(4):1–61, 2017.
[Arusoaie&Lucanu 2019] Andrei Arusoaie, Dorel Lucanu: Unification in Matching Logic. FM 2019: 502-518

Short biography: Dorel Lucanu is full professor at the Faculty of Computer science, Alexandru Ioan Cuza University of Iasi, Romania. His research interests are within the area of formal methods applied in software engineering, with focus on logics for programs (rewriting logic, matching logic), coinductive reasoning, program analysis and verification.