typetheory

Type theory is a family of formal systems in which every expression has a type, and computation proceeds by manipulating typed terms. In type theories, types classify terms and prevent ill-formed expressions; functions are defined by specifying how inputs of a given type produce outputs of another type. A distinctive feature of modern type theory is the possibility that types themselves may depend on terms, enabling precise, expressive encodings of mathematical objects and propositions.

A central idea is the Curry–Howard correspondence, which identifies propositions with types and proofs with programs. Under this view, constructing a term of a given type corresponds to proving the associated proposition. This constructive interpretation underpins the use of type theory in formal verification and computer-assisted proof.

Core systems include the simply typed lambda calculus, which enforces a fixed type structure, and its extensions such as System F with polymorphism. More expressive frameworks are Martin-Löf type theory (dependent types), the Calculus of Constructions (a higher-order, dependently typed system), and the Calculus of Inductive Constructions (CIC), which supports inductive types and forms the basis of the Coq proof assistant. To avoid paradoxes, type theories employ universe hierarchies that stratify types into levels.

In recent decades, Homotopy Type Theory (HoTT) and Univalent Foundations have integrated ideas from algebraic topology into type theory, offering new foundations for mathematics and verified results. Type theory also underpins several proof assistants, such as Coq, Agda, Idris, and Lean, and is influential in programming language design, formal verification, and the study of logic and foundations.