phase of compiler, has a connection to type theory. A prime example is Agda, a programming language which uses UTT (Luo's Unified Theory of dependent Types) for its type system. The programming language ML was developed for manipulating type theories (see LCF) and its own type system was heavily influenced by them. Linguistics Type theory is also widely used in formal theories of semantics of natural languages, especially Montague grammar and its descendants. In particular, categorial grammars and pregroup grammars extensively use type constructors to define the types (noun, verb, etc.) of words. The most common construction takes the basic types and for individuals and truth-values, respectively, and defines the set of types recursively as follows: if and are types, then so is ; nothing except the basic types, and what can be constructed from them by means of the previous clause are types. A complex type is the type of functions from entities of type to entities of type . Thus one has types like which are interpreted as elements of the set of functions from entities to truth-values, i.e. indicator functions of sets of entities. An expression of type is a function from sets of entities to truth-values, i.e. a (indicator function of a) set of sets. This latter type is standardly taken to be the type of natural language quantifiers, like everybody or nobody (Montague 1973, Barwise and Cooper 1981). Social sciences Gregory Bateson introduced a theory of logical types into the social sciences; his notions of double bind and logical levels are based on Russell's theory of types. See also Foundations of mathematics Further reading Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics. Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of 'Principia Mathematica'. Intended as a type theory counterpart of Paul Halmos's (1960) Naïve Set Theory A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. Book review Notes References External links Introductory material Type Theory at nLab, which has articles on many topics. Intuitionistic Type Theory article at the Stanford Encyclopedia of Philosophy Lambda Calculus with Types book by Henk Barendregt Calculus of Constructions / Typed Lambda Calculus textbook style