Oberwolfach References on Mathematical Software

Isabelle

Summary

Isabelle is a popular generic theorem prover developed at Cambridge University and TU Munich. Existing logics like Isabelle/HOL provide a theorem proving environment ready to use for sizable applications. Isabelle may also serve as framework for rapid prototyping of deductive systems. It comes with a large library including Isabelle/HOL (classical higher-order logic), Isabelle/HOLCF (Scott’s Logic for Computable Functions with HOL), Isabelle/FOL (classical and intuitionistic first-order logic), and Isabelle/ZF (Zermelo-Fraenkel set theory on top of FOL).

Authors

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

Vendor

Isabelle is distributed freely as Open Source Software BSD license.

Links

Status

projectstatus   officially approved by the authors

Available via

Operating Systems

Programming Languages

License

Free downloadable

Technical Category

Specialized system

Download pdf description