External Links

    Journal: J. Formalized Reasoning

    Volume 1, Issue 1

    1 -- 23Andrea Asperti, Cristian Armentano. A Page in Number Theory
    25 -- 37Concepción Vidal, Felicidad Aguado, José Luis Doncel, José María Molinelli, Gilberto Pérez. Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator
    39 -- 50André Luiz Galdino, Mauricio Ayala-Rincón. A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language
    51 -- 89Claudio Sacerdoti Coen, Enrico Tassi. A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita
    runs on