Department of Computer Science and Technology

Technical reports

The Church-Rosser theorem in Isabelle:
a proof porting experiment

Ole Rasmussen

April 1995, 27 pages

DOIhttps://doi.org/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}
}