Academic Journals Database
Disseminating quality controlled scientific knowledge

Journal of Formalized Reasoning

ISSN: 1972--5787
Publisher: CIB - University of Bologna


ADD TO MY LIST
 
An Introduction to Programming and Proving with Dependent Types in Coq

Author(s): Adam Chlipala
Volume: 3
Issue: 2
Year: 2010
Mizar in a Nutshell

Author(s): Adam Grabowski | Artur Kornilowicz | Adam Naumowicz
Volume: 3
Issue: 2
Year: 2010
An introduction to small scale reflection in Coq

Author(s): Georges Gonthier | Assia Mahboubi
Volume: 3
Issue: 2
Year: 2010
A Formal Proof of Square Root and Division Elimination in Embedded Programs

Author(s): Pierre Neron
Volume: 6
Issue: 1
Year: 2013
A formal proof of Sasaki-Murao algorithm

Author(s): Thierry Coquand | ANDERS MORTBERG | VINCENT SILES
Volume: 5
Issue: 1
Year: 2012
A proof of Bertrand's postulate

Author(s): Andrea Asperti | Wilmer Ricciotti
Volume: 5
Issue: 1
Year: 2012
A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration

Author(s): Luca Chiarabini | Olivier Danvy
Volume: 4
Issue: 1
Year: 2011
Formalizing a Proof that e is Transcendental

Author(s): Jesse Bingham
Volume: 4
Issue: 1
Year: 2011
Initial Semantics for higher-order typed syntax in Coq

Author(s): Benedikt Ahrens | Julianna Zsido
Volume: 4
Issue: 1
Year: 2011
A Formal Proof Of The Riesz Representation Theorem

Author(s): Anthony Narkawicz
Volume: 4
Issue: 1
Year: 2011
Formalization of the Integral Calculus in the PVS Theorem Prover

Author(s): Ricky Wayne Butler
Volume: 2
Issue: 1
Year: 2009
A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita

Author(s): Claudio Sacerdoti Coen | Enrico Tassi
Volume: 1
Issue: 1
Year: 2008
Basic first-order model theory in Mizar

Author(s): Marco Bright Caminati
Volume: 3
Issue: 1
Year: 2010
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure

Author(s): Geoff Sutcliffe | Christoph Benzmueller
Volume: 3
Issue: 1
Year: 2010
A New Look at Generalized Rewriting in Type Theory

Author(s): Matthieu Sozeau
Volume: 2
Issue: 1
Year: 2009
A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language

Author(s): Andre Luiz Galdino | Mauricio Ayala-Rincón
Volume: 1
Issue: 1
Year: 2008
Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator

Author(s): Concepción Vidal | Felicidad Aguado | José Luis Doncel | Jose María Molinelli | Gilberto Perez
Volume: 1
Issue: 1
Year: 2008
Sets in Coq, Coq in Sets

Author(s): Bruno Barras
Volume: 3
Issue: 1
Year: 2010
A formalized proof of Dirichlet's theorem on primes in arithmetic progression

Author(s): John Harrison
Volume: 2
Issue: 1
Year: 2009
Computing with Classical Real Numbers

Author(s): Cezary Kaliszyk | Russell O'Connor
Volume: 2
Issue: 1
Year: 2009
A Page in Number Theory

Author(s): Andrea Asperti | Cristian Armentano
Volume: 1
Issue: 1
Year: 2008
Why do you need a reservation system?      Affiliate Program