Notes on applicative matching logic

Abstract

Matching logic (ML) was developed by Grigore Roş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ş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.