More Church-Rosser Proofs (in Isabelle/HOL)

Tobias Nipkow

The proofs of the Church-Rosser theorems for beta, eta and beta+eta reduction in untyped lambda-calculus are formalized in Isabelle/HOL, an implementation of Higher Order Logic in the generic theorem prover Isabelle. For beta-reduction, both the standard proof and the variation by Takahashi are given and compared. All proofs are based on a general theory of commutating relations which supports an almost geometric style of reasoning about confluence diagrams.

(Journal version of CADE96 paper)

dvi ps


@article{Nipkow-JAR01,author={Tobias Nipkow},
title={More {Church-Rosser} Proofs (in {Isabelle/HOL})},
The corresponding Isabelle theories.