Return to Article Details Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover Download Download PDF