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

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

Author(s): Ferruccio Guidi
Volume: 5
Issue: 1
Year: 2012

A proof of Bertrand's postulate

Author(s): Andrea Asperti | Wilmer Ricciotti
Volume: 5
Issue: 1
Year: 2012

Initial Semantics for higher-order typed syntax in Coq

Author(s): Benedikt Ahrens | Julianna Zsido
Volume: 4
Issue: 1
Year: 2011

A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration

Author(s): Luca Chiarabini | Olivier Danvy
Volume: 4
Issue: 1
Year: 2011

A Formal Proof Of The Riesz Representation Theorem

Author(s): Anthony Narkawicz
Volume: 4
Issue: 1
Year: 2011

Formalizing a Proof that e is Transcendental

Author(s): Jesse Bingham
Volume: 4
Issue: 1
Year: 2011

Mizar in a Nutshell

Author(s): Adam Grabowski | Artur Kornilowicz | Adam Naumowicz
Volume: 3
Issue: 2
Year: 2010

An Introduction to Programming and Proving with Dependent Types in Coq

Author(s): Adam Chlipala
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

Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure

Author(s): Geoff Sutcliffe | Christoph Benzmueller
Volume: 3
Issue: 1
Year: 2010

Basic first-order model theory in Mizar

Author(s): Marco Bright Caminati
Volume: 3
Issue: 1
Year: 2010

Sets in Coq, Coq in Sets

Author(s): Bruno Barras
Volume: 3
Issue: 1
Year: 2010

Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets

Author(s): José Grimm
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

Formalization of the Integral Calculus in the PVS Theorem Prover

Author(s): Ricky Wayne Butler
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 formalized proof of Dirichlet's theorem on primes in arithmetic progression

Author(s): John Harrison
Volume: 2
Issue: 1
Year: 2009

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

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

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

A Page in Number Theory

Author(s): Andrea Asperti | Cristian Armentano
Volume: 1
Issue: 1
Year: 2008