Dear friends of formal proofs,
Have you ever wanted to share your proofs with other people? Did you ever need some particular formalized theory but could not find anything suitable on the web?
We are please to announce AFP
The Archive of Formal Proofs
AFP is the central repository for sharing theories written in the theorem prover Isabelle.
AFP is a source of knowledge, examples, and libraries.
AFP is organized like a journal.
Typical AFP entries are
- Mathematical theories
- Algorithm verifications
- Proof pearls
In short, anything useful or beautiful, large or small!
Science means sharing. We all need everybody's contributions!
Looking forward to a flood of theories pouring in!
Gerwin Klein, Sydney
Tobias Nipkow, Munich
Larry Paulson, Cambridge