Isabelle

What is Isabelle?

Isabelle is a platform for Interactive Theorem Proving, with standard support for the main operating-system families: Linux, Windows, Mac OS X. It is available from the mirror sites at Cambridge (UK), Munich (Germany), Sydney (Australia), Potsdam (USA).

The most prominent application of the framework is Isabelle/HOL, which is part of the main Isabelle distribution. Numerous user contributions are available from the Archive of Formal Proofs.

History

Isabelle was started in 1986 by L.C. Paulson (Cambridge), as a successor to his earlier LCF system. My own involvement in the Isabelle project goes back to 1993,  as a student of T. Nipkow at TU Munich. Isabelle is one of the main players in Interactive Theorem Proving (ITP), together with Coq, the HOL family, ACL2, and others.

Isabelle today is notable for its advanced Prover IDE, which is called Isabelle/jEdit and based on the jEdit text editor. The system integrates many tools for interactive and automated theorem proving into one environment, which works for users out-of-the box without separate installation.

My places in the Isabelle universe

  • The isabelle-users mailing list covers all aspects concerning official Isabelle releases, including Isabelle/ML tool development by users.
  • The isabelle-dev mailing list covers all aspects around ongoing development of Isabelle itself, between the official releases. In discussions it is important to refer to proper changeset ids from the Mercurial repository.
  • The Stackoverflow cummunity of Isabelle is centered around the tags isabelle, isar, jedit.
  • The Poly/ML mailing list covers all aspects of this great SML platform by David Matthews. In recent years, Poly/ML has become the most advanced SML implementation, and the mailing list a place to discuss general SML topics as well.
  • The jedit-devel maling list covers ongoing development and maintenance of the text editor that underlies the default Isabelle/PIDE front-end: Isabelle/jEdit. Note that the mailing list is connected to various trackers, which makes it a bit difficult to follow genuine discussions that happen there as well.