#### A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle

Julian Nagele, Vincent van Oostrom, and Christian Sternagel

Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 55 – 59, 2016.

##### 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.

@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}
Nach oben scrollen