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 confluence proofs.
This work is superseded by its journal version.
dvi
SpringerLink
BibTeX:
@inproceedings{Nipkow-CADE-96,author={Tobias Nipkow},
title={More {Church-Rosser} Proofs (in {Isabelle/HOL})},
booktitle={Automated Deduction --- CADE-13},
editor={M. McRobbie and J.K. Slaney},
publisher=Springer,series=LNCS,volume=1104,pages={733--747},year=1996,
url={http://www4.informatik.tu-muenchen.de/~nipkow/pubs/cade96.dvi.gz}}
The corresponding
Isabelle theories.