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.

BibTeX

@inproceedings{JNVvOCS-IWC16,
  author    = "Julian Nagele and Vincent van Oostrom and Christian Sternagel",
  title     = "A Short Mechanized Proof of the Church-Rosser Theorem by the
               Z-property for the $\lambda\beta$-calculus in Nominal Isabelle",
  booktitle = "Proceedings of the 5th International Workshop on Confluence",
  editor    = "Beniamino Accattoli and Ashish Tiwari",
  pages     = "55--59",
  year      = 2016
}