%0 Journal Article
%T Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
%A Ferruccio Guidi
%J Journal of Formalized Reasoning
%D 2012
%I University of Bologna
%X 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 refined by Kashima that, avoiding the notion of development and having a neat inductive structure, is particularly suited for formalization in theorem provers.
%K lambda calculus
%K standardization
%K confluence
%K matita
%K interactive theorem proving
%U http://jfr.unibo.it/article/view/3392