Nominal Matching Logic with Fixpoints

Matching logic is the foundation of the K semantic environment for the specification of programming languages and automated generation of evaluators and verification tools. NLML is a formalization of nominal logic, which facilitates specification and reasoning about languages with binders, as a matching logic theory. Many properties of interest are inductive, and to prove them an induction principle modulo alpha-equality is required. In this paper we show that an alpha-structural Induction Principle for any nominal binding signature can be derived in an extension of NLML with set variables and fixpoint operators. We illustrate the use of the principle to prove properties of the λ-calculus, the computation model underlying functional programming languages. The techniques generalize to other languages with binders. The proofs have been written in and generated using Metamath Zero.