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

Christian Sternagel; Julian Nagele; Vincent van Oostrom

arxiv: 1609.03139 · v1 · pith:7V3MJYHSnew · submitted 2016-09-11 · 💻 cs.LO

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

Julian Nagele , Vincent van Oostrom , Christian Sternagel This is my paper

classification 💻 cs.LO

keywords proofshortchurch-rosserisabellenominalz-propertyassistantavailable

0 comments

read the original 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.

This paper has not been read by Pith yet.

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

discussion (0)