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
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A formal language (theory) for expressing programs. Used and studied in computer science.
plain type theory:
Last revised on May 11, 2014 at 09:31:55. See the history of this page for a list of all contributions to it.