# History of Type Theory

https://en.wikipedia.org/wiki/History\_of\_type\_theory

Contents

* Russell's paradox
* 1902 and 1908 Bertrand Russell proposed various "theories of type"
* 1900 Origin of Russell's theory of types, 1900-1927
* 1908 Ramified theory of types
* The axiom of reducibility and the notion of "matrix"
* Truth tables
* Russell's doubts
* Theory of simple types
* 1944 Gödel's theory of simple types
* 1934 Curry-Howard correspondence, 1934-1969
* 1967 de Bruijn's AUTOMATH, 1967-2003
* 1971 Martin-Löf's Intuitionistic type theory, 1971-1984
* 1991 Barendregt's lambda cube

Hindley, 1969; Milner, 1978; Damas & Milner, 1982

Type theory was initially created to avoid paradoxes in a variety of _formal logics_ and _rewrite systems_. Later, type theory referred to a class of formal systems, some of which can serve as alternatives to naive set theory as a foundation of mathematics. Type theory has been tied to formal mathematics since `Principia Mathematica` and it is a very active field today, especially through the development of _proof assistants_.
