@article{Guidi_2012, title={Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover}, volume={5}, url={https://jfr.unibo.it/article/view/3392}, DOI={10.6092/issn.1972-5787/3392}, abstractNote={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.}, number={1}, journal={Journal of Formalized Reasoning}, author={Guidi, Ferruccio}, year={2012}, month={Jan.}, pages={1–25} }