| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Download |
project summary
The Archive of Formal Proofs
| The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal. Submissions are refereed. The preferred citation style is available [here]. A development version of the archive is available. |
| 2008 |
|
2008-04-05:
Recursion Theory I
Author: Michael Nedzelsky |
|
2008-02-29:
BDD Normalisation
Veronika Ortner and Norbert Schirmer |
|
2008-02-29:
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
Author: Norbert Schirmer |
|
2008-02-18
Normalization by Evaluation
Author: Klaus Aehlig and Tobias Nipkow |
|
2008-01-11:
Quantifier Elimination for Linear Arithmetic
Author: Tobias Nipkow |
| 2007 |
|
2007-12-20:
Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors
Author: Peter Lammich and Markus Müller-Olm |
|
2007-12-03:
Jinja With Threads
Author: Andreas Lochbihler |
|
2007-11-06:
Much Ado About Two
Author: Sascha Böhme |
|
2007-08-27:
Sums of Two and Four Squares
Author: Roelof Oosterhuis |
|
2007-08-27:
Fermat's Last Theorem for Exponents 3 and 4
and the Parametrisation of Pythagorean Triples
Author: Roelof Oosterhuis |
|
2007-08-16:
POPLmark Challenge Via de Bruijn Indices
Author: Stefan Berghofer |
|
2007-08-14:
First-Order Logic According to Fitting
Author: Stefan Berghofer |
|
2007-08-08:
Fundamental Properties of Valuation Theory and Hensel's Lemma
Author: Hidetsune Kobayashi |
| 2006 |
|
2006-09-09:
Hotel Key Card System
Author: Tobias Nipkow |
|
2006-08-08:
Abstract Hoare Logics
Author: Tobias Nipkow |
|
2006-05-22:
Flyspeck I: Tame Graphs
Author: Gertrud Bauer and Tobias Nipkow |
|
2006-05-16:
CoreC++
Author: Daniel Wasserrab |
|
2006-03-31:
A Theory of Featherweight Java in Isabelle/HOL
Author: J. Nathan Foster and Dimitrios Vytiniotis |
|
2006-03-15:
Instances of Schneider's generalized protocol of clock
synchronization
Author: Damián Barsotti |
|
2006-03-14:
Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality
Author: Benjamin Porter |
| 2005 |
|
2005-11-11:
Countable Ordinals
Author: Brian Huffman |
|
2005-10-12:
Fast Fourier Transform
Author: Clemens Ballarin |
|
2005-06-20:
Jive Data and Store Model
Author: Nicole Rauch and Norbert Schirmer |
|
2005-06-24:
Formalization of a Generalized Protocol for Clock Synchronization
Author: Alwen Tiu |
|
2005-06-22:
Proving the Correctness of Disk Paxos
Author: Mauro Jaskelioff and Stephan Merz |
|
2005-06-01:
Jinja is not Java
Author: Gerwin Klein and Tobias Nipkow |
|
2005-05-10:
SHA1, RSA, PSS and more
Author: Christina Lindenberg and Kai Wirt |
|
2005-04-21:
Category Theory to Yoneda's Lemma
Author: Greg O'Keefe |