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