What is Matching Logic?

For programming language semanticists:

Matching logic is a unifying foundational logic for programming languages, specification, 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.

Traditionally, concrete behaviors of programs are defined by operational semantics, while the properties of them are specified and proved using axiomatic semantics, such as Hoare logic. Unfortunately, axiomatic semantics of real languages are rather complex, so correctness proofs are necessary in order to trust the proven properties. Moreover, such proofs have to be maintained as the language changes, which is generally perceived as a burden. Ideally, we would like to have only one reference language semantics, which are used for both deriving program behaviors and verifying programs.

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 rewrite rules. Both operational behaviors and formal properties of a program are derived using the language-independent proof system of matching logic. That is, we use the same proof system to reason about all programming languages, which is different from the classic axiomatic semantics approach where different languages require their own set of proof rules (see, e.g., Hoare logic rules for a set of proof rules that were designed specifically for a simple imperative language). In conclusion, one matching logic semantics fulfills the roles of both operational and axiomatic semantics in a uniform manner.

One of the key observations made by matching logic is that program states can be represented as algebraic datatypes called configurations. A configuration contains all information of the program state, such as its current computation (i.e. the program/code), its computing context (e.g., environments, heaps, etc.), input and output buffer, and many others. Program configurations can be matched by (configuration) patterns, which are matching logic formulas with variables and constraints. A rewrite rule of a matching logic semantics has the form lhs => rhs where lhs and rhs are patterns. It specifies that all configurations matching lhs should rewrite to the configurations matching rhs, in one computation step. In this way, matching logic defines the formal semantics of a programming language by defining the set of all its configurations and then defining a transition system over the configurations using rewrite rules.

For logicians:

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. Here is a non-exhaustive list of the logics/calculi/models that are definable in matching logic:

Matching Logic

The diagram above on the right depicts the relationship among these logics/calculi/models, where arrows mean “is subsumed by” or “can be defined in”. As seen, many important logical systems can be subsumed by or defined in matching logic as its fragments and/or logical theories.

Getting Started

Matching logic is the result of a continuous 20-year effort in finding a foundation logic for formal language frameworks, such as the K language framework, and has led many research papers. Here, we select some milestone papers for starters, discuss the ongoing projects and open problems, and review some earlier papers that compare matching logic with the classic Hoare-style program verification.

Core publications

Other publications

To understand how matching logic powers formal program verification for all languages, read the following publications, where we compare our approach to program verification with the traditional Hoare-style verification approach: