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, is indexed by dblp and has an ISSN: 2150-914x. Submissions are refereed. The preferred citation style is available [here]. A development version of the archive is available as well.

 

2013

2013-04-28: Graph Theory Author: Lars Noschinski

2013-04-15: Light-weight Containers Author: Andreas Lochbihler

2013-01-31: The Correctness of Launchbury's Natural Semantics for Lazy Evaluation Author: Joachim Breitner

2013-01-19: Ribbon Proofs Author: John Wickerson

2013-01-16: Rank-Nullity Theorem in Linear Algebra Author: Jose Divasón and Jesús Aransay

2013-01-15: Kleene Algebra Author: Alasdair Armstrong, Georg Struth and Tjark Weber

2013-01-03: Computing Square Roots using the Babylonian Method Author: René Thiemann

2012

2012-11-14: A Separation Logic Framework for Imperative HOL Author: Peter Lammich and Rene Meis

2012-11-02: Open Induction Author: Mizuhito Ogawa and Christian Sternagel

2012-10-30: The independence of Tarski's Euclidean axiom Author: T. J. M. Makarios

2012-10-27: Bondy's Theorem Author: Jeremy Avigad and Stefan Hetzl

2012-09-10: Possibilistic Noninterference Author: Andrei Popescu and Johannes Hölzl

2012-08-07: Generating linear orders for datatypes Author: René Thiemann

2012-08-05: Proving the Impossibility of Trisecting an Angle and Doubling the Cube Author: Ralph Romanos and Lawrence Paulson

2012-07-27: Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model Author: Henri Debrat and Stephan Merz

2012-07-01: Logical Relations for PCF Author: Peter Gammie

2012-06-26: Type Constructor Classes and Monad Transformers Author: Brian Huffman

2012-05-29: CCS in nominal logic Author: Jesper Bengtson

2012-05-29: The pi-calculus in nominal logic Author: Jesper Bengtson

2012-05-29: Psi-calculi in Isabelle Author: Jesper Bengtson

2012-05-27: Isabelle/Circus Author: Abderrahmane Feliachi, Burkhart Wolff and Marie-Claude Gaudel

2012-05-11: Separation Algebra Author: Gerwin Klein, Rafal Kolanski and Andrew Boyton

2012-05-07: Stuttering Equivalence Author: Stephan Merz

2012-05-02: Inductive Study of Confidentiality Author: Giampaolo Bella

2012-04-26: Ordinary Differential Equations Author: Fabian Immler and Johannes Hölzl

2012-04-13: Well-Quasi-Orders Author: Christian Sternagel

2012-03-1: Abortable Linearizable Modules Author: Rachid Guerraoui, Viktor Kuncak and Giuliano Losa

2012-02-29: Executable Transitive Closures Author: René Thiemann

2012-02-06: A Probabilistic Proof of the Girth-Chromatic Number Theorem Author: Lars Noschinski

2012-01-30: Dijkstra's Shortest Path Algorithm Author: Benedikt Nordhoff and Peter Lammich

2012-01-30: Refinement for Monadic Programs Author: Peter Lammich

2012-01-03: Markov Models Author: Johannes Hölzl and Tobias Nipkow

2011

2011-11-19: A Definitional Encoding of TLA* in Isabelle/HOL Author: Gudmund Grov and Stephan Merz

2011-11-09: Efficient Mergesort Author: Christian Sternagel

2011-09-22: Pseudo Hoops Author: George Georgescu, Laurentiu Leustean and Viorel Preoteasa

2011-09-22: Algebra of Monotonic Boolean Transformers Author: Viorel Preoteasa

2011-09-22: Lattice Properties Author: Viorel Preoteasa

2011-08-26: The Myhill-Nerode Theorem Based on Regular Expressions Author: Chunhan Wu, Xingyuan Zhang and Christian Urban

2011-08-19: Gauss-Jordan Elimination for Matrices Represented as Functions Author: Tobias Nipkow

2011-07-21: Maximum Cardinality Matching Author: Christine Rizkallah

2011-05-17: Knowledge-based programs Author: Peter Gammie

2011-04-01: The General Triangle Is Unique Author: Joachim Breitner

2011-03-14: Executable Transitive Closures of Finite Relations Author: Christian Sternagel and René Thiemann

2011-02-23: Infinite Lists Author: David Trachtenherz

2011-02-23: AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics Author: David Trachtenherz

2011-02-23: Interval Temporal Logic on Natural Numbers Author: David Trachtenherz

2011-02-07: Lightweight Java Author: Rok Strniša and Matthew Parkinson

2011-01-10: RIPEMD-160 Author: Fabian Immler

2011-01-08: Lower Semicontinuous Functions Author: Bogdan Grechuk

2010

2010-12-17: Hall's Marriage Theorem Author: Dongchen Jiang and Tobias Nipkow

2010-11-16: Shivers' Control Flow Analysis Author: Joachim Breitner

2010-10-28: Functional Binomial Queues Author: René Neumann

2010-10-28: Binomial Heaps and Skew Binomial Heaps Author: Rene Meis, Finn Nielsen and Peter Lammich

2010-10-28: Finger Trees Author: Benedikt Nordhoff, Stefan Körner and Peter Lammich

2010-08-29: Strong Normalization of Moggis's Computational Metalanguage Author: Christian Doczkal

2010-08-10: Executable Multivariate Polynomials Author: Christian Sternagel and René Thiemann

2010-08-08: Formalizing Statecharts using Hierarchical Automata Author: Steffen Helke and Florian Kammüller

2010-06-24: Free Groups Author: Joachim Breitner

2010-06-20: Category Theory Author: Alexander Katovsky

2010-06-17: Executable Matrix Operations on Matrices of Arbitrary Dimensions Author: Christian Sternagel and René Thiemann

2010-06-14: Abstract Rewriting Author: Christian Sternagel and René Thiemann

2010-05-28: Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement Author: Viorel Preoteasa and Ralph-Johan Back

2010-05-28: Semantics and Data Refinement of Invariant Based Programs Author: Viorel Preoteasa and Ralph-Johan Back

2010-05-22: A Complete Proof of the Robbins Conjecture Author: Matthew Wampler-Doty

2010-05-12: Regular Sets and Expressions Author: Alexander Krauss and Tobias Nipkow

2010-04-30: Locally Nameless Sigma Calculus Author: Ludovic Henrio, Florian Kammüller, Bianca Lutz and Henry Sudhof

2010-03-29: Free Boolean Algebra Author: Brian Huffman

2010-03-23: Information Flow Noninterference via Slicing Author: Daniel Wasserrab

2010-02-20: List Index Author: Tobias Nipkow

2010-02-12: Coinductive Author: Andreas Lochbihler

2009

2009-12-09: 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-25: Tree Automata Author: Peter Lammich

2009-11-25: Collections Framework Author: Peter Lammich, Andreas Lochbihler and Thomas Tuerk

2009-11-22: Perfect Number Theorem Author: Mark Ijbema

2009-11-13: 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-01: Ordinals and Cardinals Author: Andrei Popescu

2009-08-28: Invertibility in Sequent Calculi Author: Peter Chapman

2009-08-04: An Example of a Cofinitary Group in Isabelle/HOL Author: Bart Kastermans

2009-05-06: Code Generation for Functions as Data Author: Andreas Lochbihler

2009-04-29: Stream Fusion Author: Brian Huffman

2008

2008-12-12: A Bytecode Logic for JML and Types Author: Lennart Beringer and Martin Hofmann

2008-11-10: Secure information flow and program logics Author: Lennart Beringer and Martin Hofmann

2008-11-09: Some classical results in Social Choice Theory Author: Peter Gammie

2008-11-07: Fun With Tilings Author: Tobias Nipkow and Lawrence Paulson

2008-10-15: The Textbook Proof of Huffman's Algorithm Author: Jasmin Christian Blanchette

2008-09-16: Towards Certified Slicing Author: Daniel Wasserrab

2008-09-02: A Correctness Proof for the Volpano/Smith Security Typing System Author: Gregor Snelting and Daniel Wasserrab

2008-09-01: Arrow and Gibbard-Satterthwaite Author: Tobias Nipkow

2008-08-26: Fun With Functions Author: Tobias Nipkow

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 Author: 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-14: 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-12: Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples Author: Roelof Oosterhuis

2007-08-12: Sums of Two and Four Squares Author: Roelof Oosterhuis

2007-08-08: Fundamental Properties of Valuation Theory and Hensel's Lemma Author: Hidetsune Kobayashi

2007-08-02: POPLmark Challenge Via de Bruijn Indices Author: Stefan Berghofer

2007-08-02: First-Order Logic According to Fitting Author: Stefan Berghofer

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-15: 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-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-20: Jive Data and Store Model Author: Nicole Rauch and Norbert Schirmer

2005-06-01: Jinja is not Java Author: Gerwin Klein and Tobias Nipkow

2005-05-02: SHA1, RSA, PSS and more Author: Christina Lindenberg and Kai Wirt

2005-04-21: Category Theory to Yoneda's Lemma Author: Greg O'Keefe

2004

2004-12-09: File Refinement Author: Karen Zee and Viktor Kuncak

2004-11-19: Integration theory and random variables Author: Stefan Richter

2004-09-28: A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic Author: Tom Ridge

2004-09-20: Completeness theorem Author: James Margetson and Tom Ridge

2004-09-20: Ramsey's theorem, infinitary version Author: Tom Ridge

2004-07-09: Compiling Exceptions Correctly Author: Tobias Nipkow

2004-06-24: Depth First Search Author: Toshiaki Nishihara and Yasuhiko Minamide

2004-05-18: Groups, Rings and Modules Author: Hidetsune Kobayashi, L. Chen and H. Murao

2004-04-26: Topology Author: Stefan Friedrich

2004-04-26: Lazy Lists II Author: Stefan Friedrich

2004-04-05: Binary Search Trees Author: Viktor Kuncak

2004-03-30: Functional Automata Author: Tobias Nipkow

2004-03-19: AVL Trees Author: Tobias Nipkow and Cornelia Pusch

2004-03-19: Mini ML Author: Wolfgang Naraschewski and Tobias Nipkow