Isabelle is a proof assistant. Its main application is HOL. Related proof assistants are HOL4, HOL Light, HOL Zero, and ProofPower. These are programmed, as Isabelle itself, in ML. In contrast to other proof assistants, Isabelle is based on classical set theoretic foundations. The Archive of Formal Proofs is an online library of proofs formalized in Isabelle.

Other proof assistants


  • T. Nipkow, L. Paulson, M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, Springer (2002)

  • T. Nipkow, G. Klein. Concrete Semantics with Isabelle/HOL, Springer (2014) (web)

  • Florian Rabe and Mihnea Iancu, A Formalized Set-Theoretical Semantics of Isabelle/HOL (pdf)

category: software

Last revised on May 20, 2019 at 09:39:33. See the history of this page for a list of all contributions to it.