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
basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A project for formalization of parts of mathematics (formal proof) in formal languages supported by proof assistants (particularly in Coq).
Thierry Coquand, ForMath: Formalisation of Mathematics research project (web)
Eelis van der Weegen, Bas Spitters, Robbert Krebbers, Matthieu Sozeau, Tom Prince, Jelle Herold,
Math Classes, Coq Library for basic mathematical structures (web)
Last revised on June 18, 2019 at 10:31:36. See the history of this page for a list of all contributions to it.