Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
We present a formalization of pure lambda-calculus for the Matita interactive theorem prover, including the proofs of two relevant results in reduction theory: the confluence theorem and the standardization theorem. The proof of the latter is based on a new approach recently introduced by Xi and ref...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2012-01-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | http://jfr.unibo.it/article/view/3392 |