Contents

Idea

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

Original articles:

• 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, §5 of: A Formulation of the Simple Theory of Types, The Journal of Symbolic Logic 5 2 (1940) 56-68 [doi:10.2307/2266170]

Textbook accounts: