Type Theory

The name type theory can be used to refer to a number of logical systems. Most of them have one thing in common: they attempt to separate or stratify the construction of mathematical objects into types, so that paradoxes and illicit/improper use can be avoided.

The earliest type theories seem to have been developed by Bertrand Russell, with a view to avoiding constructions like Russell's paradox by only writing down well-typed mathematical expressions.

Soon thereafter, Church developed the simply-typed \lambda-calculus, which is also known as simple type theory.

Following that, Girard developed System F, a system of polymorphic types which is also known as polymorphic \lambda-calculus, or polymorphic type theory.

All of the above - and many more - are type theories. However, nowadays the programming language community uses the term type theory to almost exclusively refer to Martin-Löf Type Theory. Whether this includes things like the Calculus of Constructions is up for debate.

References

• For a generic overview, see the entry on type theory in the Stanford encyclopedia on philosophy.