Notes on applicative matching logic

TL;DR

This paper introduces applicative matching logic (AML), a functional variant of matching logic, providing foundational definitions and results to facilitate reasoning about programming language semantics.

Contribution

It presents the basic theory and definitions of AML, a recent functional extension of matching logic, expanding the tools for formal semantics and program reasoning.

Findings

Defines the core concepts of AML

Establishes foundational results for AML

Provides an introductory framework for AML

Abstract

Matching logic (ML) was developed by Grigore Ro\c{s}u and collaborators as a logic for defining the formal semantics of programming languages and for specifying and reasoning about the behavior of programs. These lecture notes present basic definitions and results on applicative matching logic (AML), a functional variant of ML introduced recently by Xiaohong Chen and Grigore Ro\c{s}u. They can be used as an introductory text in the theory of AML. Monk's textbook on mathematical logic has an enormous influence on the notes.