A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the $\lambda \beta$-calculus in Nominal Isabelle

Abstract

We present a short proof of the Church-Rosser property for the lambda-calculus enjoying two distinguishing features: Firstly, it employs the Z-property, resulting in a short and elegant proof; and secondly, it is formalized in the nominal higher-order logic available for the proof assistant Isabelle/HOL.

5th International Workshop on Confluence

References in corpus (1)

• General Bindings and Alpha-Equivalence in Nominal Isabelle

Cited by in corpus (1)

• Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS