Matching logic explained

Xiaohong Chen, Dorel Lucanu, Grigore Roşu

Research output: Contribution to journalArticlepeer-review


Matching logic was recently proposed as a unifying logic for specifying and reasoning about static structure and dynamic behavior of programs. In matching logic, patterns and specifications are used to uniformly represent mathematical domains (such as numbers and Boolean values), datatypes, and transition systems, whose properties can be reasoned about using one fixed matching logic proof system. In this paper we give a tutorial of matching logic. We use a suite of examples to explain the basic concepts of matching logic and show how to capture many important mathematical domains, datatypes, and transition systems using patterns and specifications. We put emphasis on the general principles of induction and coinduction in matching logic and show how to do inductive and coinductive reasoning about datatypes and codatatypes. To encourage the future tools development for matching logic, we propose and use throughout the paper a human-readable formal syntax to write specifications in a modular and compact way.

Original languageEnglish (US)
Article number100638
JournalJournal of Logical and Algebraic Methods in Programming
StatePublished - Apr 2021


  • (co)inductive data types
  • (co)monad specification
  • Dependent types
  • Matching logic
  • Program logics
  • Specification of transition systems

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Software
  • Logic
  • Computational Theory and Mathematics


Dive into the research topics of 'Matching logic explained'. Together they form a unique fingerprint.

Cite this