In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that were proposed as foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory. Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's Calculus of Inductive Constructions. History Type theory was created to avoid a paradox in a mathematical foundation based on naive set theory and formal logic. Russell's paradox, which was discovered by Bertrand Russell, existed because a set could be defined using "all possible sets", which included itself. Between 1902 and 1908, Bertrand Russell proposed various "theories of type" to fix the problem. By 1908 Russell arrived at a "ramified" theory of types together with an "axiom of reducibility" both of which featured prominently in Whitehead and Russell's Principia Mathematica published between 1910 and 1913. This system avoided Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical entity to a type. Entities of a given type are built exclusively of subtypes of that type, thus preventing an entity from being defined using itself. Russell's theory of types ruled out the possibility of a set being a member of itself. Types were not always used in logic. There were other techniques to avoid Russell's paradox. Types did gain a hold when used with one particular logic, Alonzo Church's lambda calculus. The most famous early example is Church's simply typed lambda calculus. Church's theory of types helped the formal system avoid the Kleene–Rosser paradox that afflicted the original untyped lambda calculus. Church demonstrated that it could serve as a foundation of mathematics and it was referred to as a higher-order logic. The phrase "type theory" now generally refers to a typed system based around lambda calculus. One influential system is Per Martin-Löf's intuitionistic type theory, which was proposed as a foundation for constructive mathematics. Another is Thierry Coquand's calculus of constructions, which is used as the foundation by Coq, Lean, and other "proof assistants" (computerized proof writing programs). Type theories are an area of active research, as demonstrated by homotopy type theory. Introduction There are many type theories, which makes it difficult to produce a comprehensive taxonomy;