Technical reports

# The Church-Rosser theorem in Isabelle:

a proof porting experiment

**Ole Rasmussen**

April 1995, 27 pages

**DOI:** 10.48456/tr-364

## Abstract

This paper describes a proof of the Church-Rosser theorem for the pure lambda-calculus formalised in the Isabelle theorem prover. The initial version of the proof is ported from a similar proof done in the Coq proof assistant by Girard Huet, but a number of optimisations have been performed. The development involves the introduction of several inductive and recursive definitions and thus gives a good presentation of the inductive package of Isabelle.

## Full text

PS (0.1 MB)

## BibTeX record

@TechReport{UCAM-CL-TR-364, author = {Rasmussen, Ole}, title = {{The Church-Rosser theorem in Isabelle: a proof porting experiment}}, year = 1995, month = apr, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-364.ps.gz}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-364}, number = {UCAM-CL-TR-364} }