| 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 and has an ISSN: 2150-914x. 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. |
| 2009 |
|
2009-12-10:
A Fast SAT Solver for Isabelle in Standard ML
Author: Armin Heller |
|
2009-12-03:
Formalizing the Logic-Automaton Connection
Author: Stefan Berghofer and Markus Reiter |
|
2009-11-29:
Tree Automata
Author: Peter Lammich (peter lammich at uni-muenster de) |
|
2009-11-28:
Collections Framework
Author: Peter Lammich (peter lammich at uni-muenster de) |
|
2009-11-24:
Perfect Number Theorem
Author: Mark IJbema (ijbema at fmf nl) |
|
2009-11-19:
Backing up Slicing: Verifying the Interprocedural
Two-Phase Horwitz-Reps-Binkley Slicer
Author: Daniel Wasserrab |
|
2009-10-30:
The Worker/Wrapper Transformation
Author: Peter Gammie |
|
2009-09-07:
Ordinals and Cardinals
Author: Andrei Popescu |
|
2009-09-01:
Invertibility in Sequent Calculi
Author: Peter Chapman |
|
2009-08-04:
An Example of a Cofinitary Group in Isabelle/HOL
Author: Bart Kastermans |
|
2009-05-11:
Stream Fusion
Author: Brian Huffman |
|
2009-05-06:
Code Generation for Functions as Data
Author: Andreas Lochbihler |
| 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 |