nLab Isabelle

Idea

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.

Related entries

proof assistants:

based on plain type theory/set theory:

• Metamath

• Mizar, NuPRL, Isabelle, HOL

based on dependent type theory/homotopy type theory:

• Coq, Agda, Lean, Arend

based on cubical type theory:

• cubicaltt

• redtt

• yacctt

• RedPRL

• Cubical Agda

  • library and demos

  • 1lab (cross-linked reference resource)

based on modal type theory:

• Agda-flat: installation instructions

based on simplicial type theory:

• Rzk

For monoidal category theory:

• DisCoPy

For higher category theory:

• opetopic type theory

• Globular, homotopy.io

projects for formalization of mathematics with proof assistants:

• Archive of Formal Proofs (using Isabelle)

• ForMath project (using Coq)

• MathScheme

• UniMath project (using Coq and Agda)

• Xena project (using Lean)

Other proof assistants

• Andromeda

Historical projects that died out:

• The QED Project

Links

• Wikipedia, Isabelle (proof assistant)

• Isabelle homepage

• a tutorial webpage

• the Archive of Formal Proofs webpage

• The Isabelle2014 Library

References

• 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)

Implementation of homotopy type theory in Isabelle:

• Joshua Chen, An Implementation of Homotopy Type Theory in Isabelle/Pure (arXiv:1911.00399, github:jaycech3n/Isabelle-HoTT)

category: software