We present a formalization of pure ?-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 refined by Kashima that, avoiding the notion of development and having a neat inductive structure, is particularly suited for formalization in theorem provers.
@article{3392,
title = {Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover},
journal = {Journal of Formalized Reasoning},
volume = {5},
year = {2012},
doi = {10.6092/issn.1972-5787/3392},
language = {EN},
url = {http://dml.mathdoc.fr/item/3392}
}
Guidi, Ferruccio. Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover. Journal of Formalized Reasoning, Tome 5 (2012) . doi : 10.6092/issn.1972-5787/3392. http://gdmltest.u-ga.fr/item/3392/