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.