In mathematics, logic, and computer science, a **type system** is a formal system in which every term has a "type" which defines its meaning and the operations that may be performed on it. **Type theory** is the academic study of type systems.

- History
- Basic concepts
- Type, term, value
- Typing environment, type assignment, type judgement
- Rewriting rules, conversion, reduction
- Type rules
- Decision problems
- Type checking
- Typability
- Type inhabitation
- Interpretations of type theory
- Intuitionistic logic
- Category theory
- Difference from set theory
- Optional features
- Dependent types
- Equality types 2
- Inductive types
- Universe types
- Computational component
- Type theories
- Major
- Minor
- Active
- Practical impact
- Programming languages
- Mathematical foundations
- Proof assistants
- Linguistics
- Social sciences
- Relation to category theory
- See also
- Notes
- References
- Further reading
- External links

Some type theories serve as alternatives to set theory as a foundation of mathematics. Two well-known such theories are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory.

Type theory was created to avoid paradoxes in previous foundations such as naive set theory, formal logics and rewrite systems.

Type theory is closely related to, and in some cases overlaps with, computational type systems, which are a programming language feature used to reduce bugs and facilitate certain compiler optimizations.

Between 1902 and 1908 Bertrand Russell proposed various "theories of type" in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox. 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. They attempted to resolve Russell's paradox by first creating a hierarchy of types, then assigning each concrete mathematical (and possibly other) entity to a type. Entities of a given type are built exclusively from entities of those types that are lower in their hierarchy, thus preventing an entity from being assigned to itself.

In the 1920s, Leon Chwistek and Frank P. Ramsey proposed an unramified type theory, now known as the "theory of simple types" or simple type theory, which collapsed the hierarchy of the types in the earlier ramified theory and as such did not require the axiom of reducibility.

The common usage of "type theory" is when those types are used with a term rewrite system. The most famous early example is Alonzo Church's simply typed lambda calculus. Church's theory of types^{ [1] } 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.

Some other type theories include Per Martin-Löf's intuitionistic type theory, which has been the foundation used in some areas of constructive mathematics. Thierry Coquand's calculus of constructions and its derivatives are the foundation used by Coq, Lean, and others. The field is an area of active research, as demonstrated by homotopy type theory.

The contemporary presentation of type systems in the context of type theory has been made systematic by a conceptual framework introduced by Henk Barendregt.^{ [2] }

In a system of type theory, a * term * is opposed to a *type*. For example, 4, 2 + 2, and are all separate terms with the type nat for natural numbers. Traditionally, the term is followed by a colon and its type, such as 2 : nat - this means that the number 2 is of type nat. Beyond this opposition and syntax, little can be said about types in this generality, but often, they are interpreted as some kind of collection (not necessarily sets) of the *values* that the term might evaluate to. It is usual to denote terms by e and types by τ. How terms and types are shaped depends on the particular type system and is made precise by some syntax and additional restrictions of well-formedness.

Typing usually takes place in some *context* or *environment* denoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called an *assignment*. The context completes the above opposition. Together they form a * judgement * denoted .

Type theories have explicit computation and it is encoded in rules for * rewriting * terms. These are called *conversion rules* or, if the rule only works in one direction, a * reduction rule*. For example, and are syntactically different terms, but the former reduces to the latter. This reduction is written . These rules also establish corresponding equivalences between the terms, written .

The term reduces to . Since cannot be reduced further, it is called a *normal form*. Various systems of typed lambda calculus including the simply typed lambda calculus, Jean-Yves Girard's System F, and Thierry Coquand's calculus of constructions are * strongly normalizing *. In such systems, a successful type check implies a termination proof of the term.

Based on the judgements and equivalences type inference rules can be used to describe how a type system assigns a type to syntactic constructions (terms), much like in natural deduction. To be meaningful, conversion and type rules are usually closely related as in e.g. by a subject reduction property, which might establish a part of the soundness of a type system.

A type system is naturally associated with the decision problems of type checking, typability, and type inhabitation.^{ [3] }

The decision problem of *type checking* (abbreviated by ) is:

- Given a type environment , a term , and a type , decide whether the term can be assigned the type in the type environment .

Decidability of type checking means that type safety of any given program text (source code) can be verified.

The decision problem of *typability* (abbreviated by ) is:

- Given a term , decide whether there exists a type environment and a type such that the term can be assigned the type in the type environment .

A variant of typability is *typability wrt. a type environment* (abbreviated by ), for which a type environment is part of the input. If the given term does not contain external references (such as free term variables), then typability coincides with typability wrt. the empty type environment.

Typability is closely related to type inference. Whereas typability (as a decision problem) addresses the existence of a type for a given term, type inference (as a computation problem) requires an actual type to be computed.

The decision problem of *type inhabitation* (abbreviated by ) is:

- Given a type environment and a type , decide whether there exists a term that can be assigned the type in the type environment .

Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.

The opposition of terms and types can also be views as one of *implementation* and *specification*. By program synthesis (the computational counterpart of) type inhabitation (see below) can be used to construct (all or parts of) programs from specification given in form of type information.^{ [4] }

Type theory is closely linked to many fields of active research. Most particular, the Curry–Howard correspondence provides a deep isomorphism between intuitionistic logic, typed lambda calculus and cartesian closed categories.

Beside the view of types as collection of values of a term, type theory offers a second interpretation of the opposition of term and types. Types can be seen as propositions and terms as proofs. In this way of reading a typing, a function type is viewed as an implication, i.e. as the proposition, that follows from .

The internal language of the cartesian closed category is the simply typed lambda calculus. This view can be extended to other typed lambda calculi. Certain Cartesian closed categories, the topoi, have been proposed as a general setting for mathematics, instead of traditional set theory.

There are many different set theories and many different systems of type theory, so what follows are generalizations.

- Set theory is built on top of logic. It requires a separate system like predicate logic underneath it. In type theory, concepts like "and" and "or" can be encoded as types in the type theory itself.
- In set theory, an element is not restricted to one set. In type theory, terms (generally) belong to only one type. (Where a subset would be used, type theory tends to use a predicate function that returns true if the term is in the subset and returns false if the value is not. The union of two types can be defined as a new type called a sum type, which contains new terms.)
- Set theory usually encodes numbers as sets. (0 is the empty set, 1 is a set containing the empty set, etc. See Set-theoretic definition of natural numbers.) Type theory can encode numbers as functions using Church encoding or more naturally as inductive types. Inductive types create new constants for the successor function and zero, closely resembling Peano's axioms.
- Type theory has a simple connection to constructive mathematics through the BHK interpretation. It can be connected to logic by the Curry–Howard isomorphism. And some type theories are closely connected to Category theory.

A **dependent type** is a type that depends on a term or another type. Thus, the type returned by a function may depend on the argument to the function.

For example, a list of s of length 4 may be a different type than a list of s of length 5. In a type theory with dependent types, it is possible to define a function that takes a parameter "n" and returns a list containing "n" zeros. Calling the function with 4 would produce a term with a different type than if the function was called with 5.

Another example is the type consisting of the proofs that the argument term has a certain property, such as the term of type, e.g., a given natural number, is prime. See Curry-Howard Correspondence.

Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like Idris, ATS, Agda and Epigram.

Many systems of type theory have a type that represents equality of types and of terms. This type is different from convertibility, and is often denoted **propositional equality**.

In intuitionistic type theory, the equality type (also called the identity type) is known as for identity. There is a type when is a type and and are both terms of type . A term of type is interpreted as meaning that is equal to .

In practice, it is possible to build a type but there will not exist a term of that type. In intuitionistic type theory, new terms of equality start with reflexivity. If is a term of type , then there exists a term of type . More complicated equalities can be created by creating a reflexive term and then doing a reduction on one side. So if is a term of type , then there is a term of type and, by reduction, generate a term of type . Thus, in this system, the equality type denotes that two values of the same type are convertible by reductions.

Having a type for equality is important because it can be manipulated inside the system. There is usually no judgement to say two terms are *not* equal; instead, as in the Brouwer–Heyting–Kolmogorov interpretation, we map to , where is the bottom type having no values. There exists a term with type , but not one of type .

Homotopy type theory differs from intuitionistic type theory mostly by its handling of the equality type.

A system of type theory requires some basic terms and types to operate on. Some systems build them out of functions using Church encoding. Other systems have **inductive types**: a set of base types and a set of type constructors that generate types with well-behaved properties. For example, certain recursive functions called on inductive types are guaranteed to terminate.

**Coinductive types** are infinite data types created by giving a function that generates the next element(s). See Coinduction and Corecursion.

** Induction-induction ** is a feature for declaring an inductive type and a family of types which depends on the inductive type.

** Induction recursion ** allows a wider range of well-behaved types, allowing the type and recursive functions operating on it to be defined at the same time.

Types were created to prevent paradoxes, such as Russell's paradox. However, the motives that lead to those paradoxes—being able to say things about all types—still exist. So, many type theories have a "universe type", which contains all *other* types (and not itself).

In systems where you might want to say something about universe types, there is a hierarchy of universe types, each containing the one below it in the hierarchy. The hierarchy is defined as being infinite, but statements must only refer to a finite number of universe levels.

Type universes are particularly tricky in type theory. The initial proposal of intuitionistic type theory suffered from Girard's paradox.

Many systems of type theory, such as the simply-typed lambda calculus, intuitionistic type theory, and the calculus of constructions, are also programming languages. That is, they are said to have a "computational component". The computation is the reduction of terms of the language using rewriting rules.

A system of type theory that has a well-behaved computational component also has a simple connection to constructive mathematics through the BHK interpretation.

Non-constructive mathematics in these systems is possible by adding operators on continuations such as call with current continuation. However, these operators tend to break desirable properties such as canonicity and parametricity.

- Simply typed lambda calculus which is a higher-order logic;
- intuitionistic type theory;
- system F;
- LF is often used to define other type theories;
- calculus of constructions and its derivatives.

- Automath;
- ST type theory;
- UTT (Luo's Unified Theory of dependent Types)
- some forms of combinatory logic;
- others defined in the lambda cube;
- others under the name typed lambda calculus;
- others under the name pure type system.

- Homotopy type theory is being researched.

There is extensive overlap and interaction between the fields of type theory and type systems. Type systems are a programming language feature designed to identify bugs. Any static program analysis, such as the type checking algorithms in the semantic analysis 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.

The first computer proof assistant, called Automath, used type theory to encode mathematics on a computer. Martin-Löf specifically developed intuitionistic type theory to encode *all* mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations using homotopy type theory.

Mathematicians working in category theory already had difficulty working with the widely accepted foundation of Zermelo–Fraenkel set theory. This led to proposals such as Lawvere's Elementary Theory of the Category of Sets (ETCS).^{ [5] } Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) and algebraic topology (specifically homotopy).

Much of the current research into type theory is driven by proof checkers, interactive proof assistants, and automated theorem provers. Most of these systems use a type theory as the mathematical foundation for encoding proofs, which is not surprising, given the close connection between type theory and programming languages:

- LF is used by Twelf, often to define other type theories;
- many type theories which fall under higher-order logic are used by the HOL family of provers and PVS;
- computational type theory is used by NuPRL;
- calculus of constructions and its derivatives are used by Coq, Matita, and Lean;
- UTT (Luo's Unified Theory of dependent Types) is used by Agda which is both a programming language and proof assistant

Many type theories are supported by LEGO and Isabelle. Isabelle also supports foundations besides type theories, such as ZFC. Mizar is an example of a proof system that only supports set theory.

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).

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.

Although the initial motivation for category theory was far removed from foundationalism, the two fields turned out to have deep connections. As John Lane Bell writes: "In fact categories can *themselves* be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (or sorts), i.e. "Roughly speaking, a category may be thought of as a type theory shorn of its syntax." A number of significant results follow in this way:^{ [6] }

- cartesian closed categories correspond to the typed λ-calculus (Lambek, 1970);
- C-monoids (categories with products and exponentials and one non-terminal object) correspond to the untyped λ-calculus (observed independently by Lambek and Dana Scott around 1980);
- locally cartesian closed categories correspond to Martin-Löf type theories (Seely, 1984).

The interplay, known as categorical logic, has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.

- Data type for concrete types of data in programming
- Domain theory
- Type (model theory)
- Type system for a more practical discussion of type systems for programming languages
- Univalent foundations

- ↑ Church, Alonzo (1940). "A formulation of the simple theory of types".
*The Journal of Symbolic Logic*.**5**(2): 56–68. doi:10.2307/2266170. JSTOR 2266170. - ↑ Barendregt, Henk (1991). "Introduction to generalized type systems".
*Journal of Functional Programming*.**1**(2): 125–154. doi:10.1017/s0956796800020025. hdl: 2066/17240 . ISSN 0956-7968. - ↑ Henk Barendregt; Wil Dekkers; Richard Statman (20 June 2013).
*Lambda Calculus with Types*. Cambridge University Press. p. 66. ISBN 978-0-521-76614-2. - ↑ Heineman, George T.; Bessai, Jan; Düdder, Boris; Rehof, Jakob (2016). "A long and winding road towards modular synthesis".
*Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques*. ISoLA 2016. Lecture Notes in Computer Science.**9952**. Springer. pp. 303–317. doi:10.1007/978-3-319-47166-2_21. - ↑ ETCS in
*nLab* - ↑ Bell, John L. (2012). "Types, Sets and Categories" (PDF). In Kanamory, Akihiro (ed.).
*Sets and Extensions in the Twentieth Century*. Handbook of the History of Logic.**6**. Elsevier. ISBN 978-0-08-093066-4.

In logic and proof theory, **natural deduction** is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.

In programming language theory and proof theory, the **Curry–Howard correspondence** is the direct relationship between computer programs and mathematical proofs.

**Intuitionistic type theory** is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.

A **typed lambda calculus** is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered. From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus, but from another point of view, they can also be considered the more fundamental theory and *untyped lambda calculus* a special case with only one type.

In type theory, a **type rule** is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well typed and what type expressions have. A prototypical example of the use of type rules is in defining type inference in the simply typed lambda calculus, which is the internal language of Cartesian closed categories.

In mathematical logic and computer science, the **calculus of constructions** (**CoC**) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Coq and other proof assistants.

**System F**, also known as the (**Girard–Reynolds**) **polymorphic lambda calculus** or the **second-order lambda calculus**, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974).

In mathematical logic and type theory, the **λ-cube** is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to:

The **cut-elimination theorem** is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen in his landmark 1934 paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively. The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the **cut rule** also possesses a **cut-free proof**, that is, a proof that does not make use of the cut rule.

**Bunched logic** is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about *resource composition*, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.

The **SKI combinator calculus** is a combinatory logic, a computational system that may be perceived as a reduced version of the untyped lambda calculus. It can be thought of as a computer programming language, though it is not convenient for writing software. Instead, it is important in the mathematical theory of algorithms because it is an extremely simple Turing complete language. It was introduced by Moses Schönfinkel and Haskell Curry.

Greek letters are used in mathematics, science, engineering, and other areas where mathematical notation is used as symbols for constants, special functions, and also conventionally for variables representing certain quantities. In these contexts, the capital letters and the small letters represent distinct and unrelated entities. Those Greek letters which have the same form as Latin letters are rarely used: capital A, B, E, Z, H, I, K, M, N, O, P, T, Y, X. Small ι, ο and υ are also rarely used, since they closely resemble the Latin letters i, o and u. Sometimes font variants of Greek letters are used as distinct symbols in mathematics, in particular for ε/ϵ and π/ϖ. The archaic letter digamma (Ϝ/ϝ/ϛ) is sometimes used.

In computer science and logic, a **dependent type** is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Clojure, Coq, F*, Epigram, and Idris, dependent types may help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.

The **simply typed lambda calculus**, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties.

In computer science, **Programming Computable Functions** (PCF) is a typed functional language introduced by Gordon Plotkin in 1977, based on previous unpublished material by Dana Scott. It can be considered to be an extended version of the typed lambda calculus or a simplified version of modern typed functional languages such as ML or Haskell.

In programming language semantics, **normalisation by evaluation (NBE)** is a style of obtaining the normal form of terms in the λ-calculus by appealing to their denotational semantics. A term is first *interpreted* into a denotational model of the λ-term structure, and then a canonical representative is extracted by *reifying* the denotation. Such an essentially semantic approach differs from the more traditional syntactic description of normalisation as a reductions in a term rewrite system where β-reductions are allowed deep inside λ-terms.

In type theory, a branch of mathematical logic, in a given typed calculus, the **type inhabitation problem** for this calculus is the following problem: given a type and a typing environment , does there exist a -term M such that ? With an empty type environment, such an M is said to be an inhabitant of .

A **Hindley–Milner** (**HM**) **type system** is a classical type system for the lambda calculus with parametric polymorphism. It is also known as **Damas–Milner** or **Damas–Hindley–Milner**. It was first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis.

In mathematical logic, category theory, and computer science, **kappa calculus** is a formal system for defining first-order functions.

In mathematical logic, the **intersection type discipline** is a branch of type theory encompassing type systems that use the **intersection type constructor** to assign multiple types to a single term. In particular, if a term can be assigned *both' the type and the type , then can be assigned the intersection type .* Therefore, the intersection type constructor can be used to express finite heterogeneous ad hoc polymorphism . For example, the λ-term can be assigned the type in most intersection type systems, assuming for the term variable both the function type and the corresponding argument type .

- Farmer, William M. (2008). "The seven virtues of simple type theory".
*Journal of Applied Logic*.**6**(3): 267–286. doi:10.1016/j.jal.2007.11.001.

- Aarts, C.; Backhouse, R.; Hoogendijk, P.; Voermans, E.; van der Woude, J. (December 1992). "A Relational Theory of Datatypes". Technische Universiteit Eindhoven.
- Andrews B., Peter (2002).
*An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof*(2nd ed.). Kluwer. ISBN 978-1-4020-0763-7. - Jacobs, Bart (1999).
*Categorical Logic and Type Theory*. Studies in Logic and the Foundations of Mathematics.**141**. Elsevier. ISBN 978-0-444-50170-7. Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics. - Cardelli, Luca (1996). "Type Systems". In Tucker, Allen B. (ed.).
*The Computer Science and Engineering Handbook*. CRC Press. pp. 2208–36. ISBN 9780849329098. - Collins, Jordan E. (2012).
*A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'*. Lambert Academic Publishing. hdl:11375/12315. ISBN 978-3-8473-2963-3. 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'. - Constable, Robert L. (2012) [2002]. "Naïve Computational Type Theory" (PDF). In Schwichtenberg, H.; Steinbruggen, R. (eds.).
*Proof and System-Reliability*. Nato Science Series II.**62**. Springer. pp. 213–259. ISBN 9789401004138. Intended as a type theory counterpart of Paul Halmos's (1960)*Naïve Set Theory* - Coquand, Thierry (2018) [2006]. "Type Theory".
*Stanford Encyclopedia of Philosophy*. - Thompson, Simon (1991).
*Type Theory and Functional Programming*. Addison–Wesley. ISBN 0-201-41667-0. - Hindley, J. Roger (2008) [1995].
*Basic Simple Type Theory*. Cambridge University Press. ISBN 978-0-521-05422-5. A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. Book review - Kamareddine, Fairouz D.; Laan, Twan; Nederpelt, Rob P. (2004).
*A modern perspective on type theory: from its origins until today*. Springer. ISBN 1-4020-2334-0. - Ferreirós, José; Domínguez, José Ferreirós (2007). "X. Logic and Type Theory in the Interwar Period".
*Labyrinth of thought: a history of set theory and its role in modern mathematics*(2nd ed.). Springer. ISBN 978-3-7643-8349-7. - Laan, T.D.L. (1997).
*The evolution of type theory in logic and mathematics*(PDF) (PhD). Eindhoven University of Technology. doi:10.6100/IR498552. ISBN 90-386-0531-5.

- Robert L. Constable (ed.). "Computational type theory".
*Scholarpedia*. - The TYPES Forum — moderated e-mail forum focusing on type theory in computer science, operating since 1987.
- The Nuprl Book: "Introduction to Type Theory."
- Types Project lecture notes of summer schools 2005–2008
- The 2005 summer school has introductory lectures

- Type theory in nLab, which has articles on many related topics.
- Oregon Programming Languages Summer School, many lectures and some notes.

This page is based on this Wikipedia article

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.