Abstract:
Matching logic (ML) is a minimal, foundational logic built around the notion of patterns — formulas interpreted as sets of elements — with native support for a least-fixpoint operator. Its expressive power and uniform treatment of structure and constraints make it a compelling substrate for domain-specific reasoning.
In this talk, we show how matching logic serves as a unifying foundation for inference systems across several domains. We begin with a self-contained introduction to matching logic: its syntax, semantics, and proof system. We then develop three case studies: (1) initial algebra semantics, where structural induction and primitive recursion are derived as theorems within matching logic rather than imposed as external rules; (2) rewrite-theory-generic reachability logic, where constrained constructor patterns are faithfully captured as matching logic theories; and (3) the K framework, where high-level language definitions are formally translated into matching logic theories, providing a rigorous denotational semantics for the K frontend.
Together, these results demonstrate that matching logic is a practical platform for deriving and certifying domain-specific reasoning systems within a single logical framework.
Short Bio:
Dorel Lucanu is a Romanian computer scientist and professor at the Faculty of Computer Science, Alexandru Ioan Cuza University of Iași. His work focuses on formal methods, programming languages, software engineering, logics, rewriting systems, and the interaction between AI and formal methods. He has major contributions to the development of the Circ prover and K Framework.
He earned a Ph.D. in Computer Science from the Institute of Mathematics of the Romanian Academy in 1994 and obtained habilitation-equivalent Ph.D. supervision status at Alexandru Ioan Cuza University in 2007. He has taught programming, algorithms, and formal methods in software engineering at the Faculty of Computer Science since its founding in 1992.
