Type theory organises mathematical and computational objects into categories called "types," providing both a foundation for mathematics that avoids the paradoxes of naive set theory, and the theoretical basis for the type systems of modern programming languages. A deep connection — the Curry-Howard correspondence — reveals that types are propositions, programs are proofs, and the act of writing a correct computer program is, in a rigorous sense, the same thing as constructing a mathematical proof.
In everyday computing, "types" are familiar: an integer, a string of text, a true/false value — these are different types of data, and mixing them up causes errors. Type theory applies this idea to mathematics itself, assigning every mathematical object a "type" and restricting what operations are meaningful based on types. This seemingly simple organisational move turns out to prevent the logical paradoxes (like Russell's Paradox — see the ZFC Axioms entry) that plagued naive 19th-century set theory.
Every time a compiler or interpreter rejects your code because you tried to add a number to a piece of text, it's enforcing a type discipline — an idea whose mathematical foundations trace directly to type theory. Languages like Haskell, Rust, and dependently-typed languages like Agda and Lean implement type systems whose theoretical underpinnings come directly from modern type theory. Getting the types right isn't just a programming convenience; in dependently-typed systems, it's literally the same thing as writing a mathematical proof.
Alonzo Church introduced the simply typed lambda calculus in 1940, assigning a type to every expression in his lambda calculus (the formal model of computation underlying all functional programming). Simple types prevent self-application (the lambda-calculus equivalent of a set containing itself) — and every well-typed expression in the simply typed lambda calculus is guaranteed to terminate its computation, a useful and nontrivial property.
Dependent types — types that depend on values, not just on other types — vastly increase expressive power. For example, the type "a list of exactly n integers" depends on the value n. Per Martin-Löf introduced dependent type theory in the 1970s as both a foundation for constructive mathematics and a programming language. In a dependently-typed system, you can express properties like "this sorting function returns a list in sorted order" directly in the type, and the type-checker verifies the property holds — turning type-checking into theorem-proving.
One of the most beautiful and surprising discoveries in 20th-century logic is the Curry-Howard correspondence (observed independently by Haskell Curry in 1934 and William Howard in 1969): types correspond to logical propositions, and programs (terms) of a given type correspond to proofs of the corresponding proposition. Writing a program that type-checks is exactly the same as constructing a proof. This deep bridge between computation and logic — "programs are proofs, types are propositions" — underlies the design of every modern proof assistant (Coq, Lean, Agda, Idris) and is now foundational to verified software engineering.
Homotopy type theory (HoTT), developed in the 2000s–2010s by Vladimir Voevodsky and others, extends dependent type theory with insights from algebraic topology — in particular, the idea that equality between two objects can itself carry structure (like a path between two points in a topological space). Voevodsky's Univalence Axiom (which, informally, states that isomorphic structures are equal) gives HoTT a distinctive character as a foundations of mathematics that is both computationally effective and geometrically suggestive — and is one of the most active research areas in mathematical foundations today.
Type theory is inherently constructive: to prove that something exists, you must actually construct it — a mere proof by contradiction is not sufficient. This aligns type theory with the tradition of constructive mathematics (associated with L.E.J. Brouwer's intuitionism) rather than classical mathematics. In classical logic, the law of excluded middle (every statement is either true or false) and the axiom of choice hold unconditionally; in constructive type theory, they must be explicitly assumed or derived — and many systems deliberately avoid them, maintaining the property that every proof yields an explicit computational witness.
The most practically consequential application of type theory today is in proof assistants — software that allows mathematicians to write fully formal, machine-verified proofs. Coq (now called Rocq, based on the Calculus of Inductive Constructions), Lean 4 (which uses a variant of the Calculus of Constructions with universes), Agda, and Isabelle/HOL are the leading systems. Major mathematical results verified in these systems include: the Four Colour Theorem (Coq, 2005), the Kepler Conjecture (HOL Light and Isabelle, 2014), the odd order theorem in group theory (Coq, 2012, a massive 255,000-line formalisation of a famous 1963 result), and an ongoing project to formalise Wiles's proof of Fermat's Last Theorem in Lean (begun 2024).
Vladimir Voevodsky (Fields Medal 2002, for work in algebraic geometry) became convinced in the 2000s that the foundations of mathematics needed to be made fully formal and computer-checkable to ensure correctness of complex modern proofs. This conviction led him to develop the Univalent Foundations programme, centred on homotopy type theory and implemented in the Coq proof assistant. His Univalence Axiom — which asserts that equivalent mathematical structures are genuinely equal as types — gives a clean, computationally meaningful way to work with mathematical structures up to isomorphism, directly formalising the common mathematical practice of treating isomorphic objects as identical. Voevodsky's 2013 lecture "An Experimental Library of Formalized Mathematics based on the Univalent Foundations" marked a significant step in making this programme concrete.