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
An extensional type theory proof management system.
The dialect of intuitionistic type theory used is also referred to as computational type theory.
The PRL part of the name evidently stands for “Proof Refinement Logic”.
MetaPRL: A logical framework implementation that includes (an old version of) Nuprl’s logic as a theory, and focuses on an efficient, modular tactic engine for proof automation.
RedPRL: An experimental proof assistant for a cubical variant of computational type theory.
Prototype CompLF: A tentative design for a modern, minimalistic variant of Nuprl’s logic, with an emphasis on internally reflecting the semantic judgments.
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:
Robert Constable, Stuart F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, NJ, 1986.