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 version of type theory. In practice any type theory is called a simple type theory if type formation is not indexed, that is the judgment that a type $A$ is well-formed has no other inputs. Contrast polymorphic type theory, where types depend on a context of type variables or dependent type theory, where types depend on a context of more general variables.
Bertrand Russell, Mathematical Logic as Based on the Theory of Types, American Journal of Mathematics, Vol. 30, No. 3 (Jul., 1908), pp. 222-262
Alonzo Church, A Formulation of the Simple Theory of Types, The Journal of Symbolic Logic Vol. 5, No. 2 (Jun., 1940), pp. 56-68 (JSTOR)
W. Farmer, The seven virtues of simple type theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267–286.
J. Roger Hindley, Basic Simple Type Theory, Cambridge University Press, 2008
Last revised on August 23, 2018 at 10:02:49. See the history of this page for a list of all contributions to it.