| 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]. |
| This is the development version of the AFP. It is provided as a preview of the next upcoming release and might contain entries that are currently broken and that might change without notice over time. Use at your own risk. Please refer to the release version only in citations. |
| 2008 |
|
2008-07-23:
Formal Verification of Modern SAT Solvers
Author: Filip Maric |
|
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 |