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 type theory, regarding propositions as types, a proof of a proposition is given by constructing a term of the corresponding type. This can hence be regarded as a program to compute a specific term (output).
definition/proof/program (proofs as programs)
An exposition is in
That Martin-Löf dependent type theory can be regarded also as a functional programming language by identifying proofs as programs was stressed in
of the Royal Society of London (Series A) 312 (1984), no. 1522, pp. 501–518.
Last revised on January 12, 2014 at 10:12:06. See the history of this page for a list of all contributions to it.