Dorel Lucanu
Alexandru Ioan Cuza University, Iaşi, Romania

Matching logic (ML) (http://www.matching-logic.org/) is a logic that allows to uniformly specify and reason about programming languages and properties of their programs. ML serves as the foundation of the K framework (https://kframework.org/), where the semantics of a programming language is (conceptually) represented as a ML theory and the goal is to automatically generate sound tools for the language starting from the K definition of the language. Such a tool is the K Prover (KP), a generic tool able to prove program properties expressed as reachability ML patterns. In this talk, we discuss some aspects regarding how to axiomatize programming languages as ML theories, including what kind of representation is the most suitable for proving and for proof checking.