Project partners

Isabelle is a joint project between Larry Paulson (University of Cambridge, UK) and Tobias Nipkow (Technical University of Munich, Germany).

There is an (incomplete) list of past and present projects undertaken using Isabelle.

Isabelle in your neighbourhood

Find out on the world map!

Mailing list

You may use the mailing list isabelle-users@cl.cam.ac.uk and its archive to discuss problems and results. To subscribe, contact our robot: Cl-isabelle-users-request@lists.cam.ac.uk.

Contributing theorems

Did you have to prove a lemma that should have been part of the Isabelle distribution? Send it to us!

We will collect theorems sent to isabelle-lemmas@cl.cam.ac.uk. Accepted material will be included in the Isabelle sources, with credit given to the author. Note that the Isabelle sources are distributed under the BSD license. Lemmas should be general, useful, and not too large. For larger developments you might want to consider a submission to the Archive of Formal Proofs.

The Archive of Formal Proofs (AFP)

The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in Isabelle. It is organized in the way of a scientific journal. Submissions are refereed.