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.