F. Guidi, “Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover”, JFR, vol. 5, no. 1, pp. 1–25, Jan. 2012.