| This resource is not discoverable in the library. If the resource was recently submitted, it may require some time before it becomes discoverable through this search service. | | Resource Title: | The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment
|
|---|
| Description: | This paper describes a proof of the Church-Rosser theorem for the pure -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 Gérard 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. |
|---|
|
