constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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.
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
based on cubical type theory:
1lab (cross-linked reference resource)
based on modal type theory:
based on simplicial type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq and Agda)
Xena project (using Lean)
Other proof assistants
Historical projects that died out:
Wikipedia, Isabelle (proof assistant)
Isabelle homepage
a tutorial webpage
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:
Last revised on May 26, 2020 at 11:00:16. See the history of this page for a list of all contributions to it.