# nLab simple type 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.

## References

• 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.