What is Isabelle?
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson), Technische Universität München (Tobias Nipkow) and Université Paris-Sud (Makarius Wenzel). See the Isabelle overview for a brief introduction.
Google Summer of Code
Isabelle participates in Google Summer of Code this year. We are looking for students interested in improving Isabelle. Some project suggestions can be found on our GSoC ideas page, but we encourage students to also submit their own ideas.Now available: Isabelle2011
Notable changes:
- Experimental Prover IDE based on Isabelle/Scala and jEdit.
- Coercive subtyping (configured in HOL/Complex_Main).
- HOL code generation: Scala as another target language.
- HOL: partial_function definitions.
- HOL: various tool enhancements, including Quickcheck, Nitpick, Sledgehammer, SMT integration.
- HOL: various additions to theory library, including HOL-Algebra, Imperative_HOL, Multivariate_Analysis, Probability.
- HOLCF: reorganization of library and related tools.
- HOL/SPARK: interactive proof environment for verification conditions generated by the SPARK Ada program verifier.
- Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
See also the cumulative NEWS.
Download & Support
Isabelle is distributed for free under the BSD license. It includes source and binary packages and browsable documentation, see the installation instructions.
A vast collection of Isabelle examples and applications is available from the Archive of Formal Proofs.
Support is available by ample documentation and the Isabelle community.