Vol. 5 No. 1 (2012)

Articles

• Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover

  Ferruccio Guidi

  1-25

  • PDF

• A formal proof of Sasaki-Murao algorithm

  Thierry Coquand, Anders Mörtberg, Vincent Siles

  27-36

  • PDF

• A proof of Bertrand's postulate

  Andrea Asperti, Wilmer Ricciotti

  37-57

  • PDF