**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**

In computer science a *program* is a construction of a term of a certain type (the output of the program).

Under computational trinitarianism this is essentially the same as a proof in type theory of the proposition presented by the type (see at *propositions as types* and *proofs as programs*).

Last revised on May 22, 2019 at 09:37:55. See the history of this page for a list of all contributions to it.