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


@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},
The corresponding Isabelle theories.