constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The UniMath project (short for Univalent Mathematics) on formalization of mathematics (formal proof) with emphasis on the use of the univalence axiom.
based on plain type theory/set theory:
based on dependent type theory/homotopy 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)
Xena project (using Lean)
Historical projects that died out:
Implementation in Coq:
Last revised on August 4, 2020 at 07:56:32. See the history of this page for a list of all contributions to it.