What is the Archive of Formal Projects?

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. We aim to strengthen the community and to foster the development of formal proofs. We aim to strengthen the community and to foster the development of formal proofs.

The archive is meant to provide

a resource of knowledge, examples, and libraries for users,

a large and relevant test bed of theories for Isabelle developers, and

a central, citable place for authors to publish their theories

All entries in the Archive of Formal Proof are licensed under a BSD-style License or the GNU LGPL. This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions.

Project homepage: http://afp.sourceforge.net

Projects