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
(…)
A. M. Turing. On Computable Numbers, with an Application to the Entscheidungs problem), Proceedings of the London Mathematical Society. 2 (1937) 42: 230–265. (pdf)
A. N. Kolmogorov and V. A. Uspénski. On the definition of an algorithm. Uspehi Mat. Nauk. 13 (1958), 3-28. English translation in American Mathematical Society Translations, Series II, Volume 29 (1963), pp. 217–245. (math-net.ru). Also see JSL review by Elliott Mendelson on jstor.
See also
Last revised on May 22, 2019 at 05:40:24. See the history of this page for a list of all contributions to it.