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} }