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
The Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic is a description of proofs of propositions in intuitionistic logic as functions, often computable functions, where it is also called the realizability interpretation.
This is otherwise known as the paradigm of propositions as types and proofs as programs. See there for more
Wikipedia, BHK interpretation
A. Kolmogoroff, Zur Deutung der intuitionistischen Logik , Math. Z. 35 1932 pp.58-65. (gdz)
Jean-Yves Girard, Proofs and Types
Anne Sjerp Troelstra, History of Constructivism in the Twentieth Century (1991). (pdf)
Links to many papers on realizability and related topics may be found here.
For a comment see also