A mechanical proof of the Church-Rosser theorem
- 1 June 1988
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 35 (3) , 475-522
- https://doi.org/10.1145/44483.44484
Abstract
The Church-Rosser theorem is a celebrated metamathematical result on the lambda calculus. We describe a formalization and proof of the Church-Rosser theorem that was carried out with the Boyer-Moore theorem prover. The proof presented in this paper is based on that of Tait and Martin-Löf. The mechanical proof illustrates the effective use of the Boyer-Moore theorem prover in proof checking difficult metamathematical proofs.Keywords
This publication has 4 references indexed in Scilit:
- Highlights of the history of the lambda-calculusPublished by Association for Computing Machinery (ACM) ,1982
- Combinators, λ-Terms and Proof TheoryPublished by Springer Nature ,1972
- LISP 1.5 PROGRAMMER'S MANUALPublished by Defense Technical Information Center (DTIC) ,1962
- Some properties of conversionTransactions of the American Mathematical Society, 1936