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

TL;DR

This paper provides a concise, formal proof of the Church-Rosser property for the lambda-calculus using the Z-property, formalized in Isabelle/HOL with nominal higher-order logic.

Contribution

It introduces a short, elegant proof of the Church-Rosser theorem leveraging the Z-property, formalized in a proof assistant with nominal logic.

Findings

Proof is concise and elegant due to the Z-property approach

Formalization in Isabelle/HOL ensures rigor and reproducibility

Applicable to lambda-calculus with beta-reduction

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.