External Links

    Journal: J. Formalized Reasoning

    Volume 5, Issue 1

    1 -- 25Ferruccio Guidi. Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
    27 -- 36Thierry Coquand, Anders Mörtberg, Vincent Siles. A formal proof of Sasaki-Murao algorithm
    37 -- 57Andrea Asperti, Wilmer Ricciotti. A proof of Bertrand's postulate
    runs on