cl-banner

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.

 

  PDF

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