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)
ps
BibTeX:
@article{Nipkow-JAR01,author={Tobias Nipkow},
title={More {Church-Rosser} Proofs (in {Isabelle/HOL})},
journal=JAR,volume=26,pages={51--66},year=2001}
The corresponding
Isabelle theories.