Foundations of mathematics

Type theory

A foundation for mathematics and computation where every term carries a type, used in proof assistants.

IntuitionEvery value has a label

In most programming languages, $3$ is an `int` and `"hello"` is a `string` — the compiler rejects `3 + "hello"` before the program ever runs. Type theory turns this everyday idea into a foundation for all of mathematics: instead of starting from sets and membership ( $x \in A$ ), start from terms and types ( $t : A$ , " $t$ has type $A$ "). Remarkably, once types are rich enough, a type can encode a mathematical proposition, and a term of that type becomes a proof — programs and proofs become the same kind of object.

A typing derivation as a tree: each node is a judgment

\Gamma \vdash t : A

, each edge a typing rule connecting a term to its subterms.

UndergraduateSimply typed lambda calculus

Definition: Typing judgment

A typing judgment $\Gamma \vdash t : A$ says "in context $\Gamma$ (a list of variable-type pairs $x_1:A_1,\dots,x_n:A_n$ ), term $t$ has type $A$ ". The core rules: a variable has whatever type its context assigns it; an abstraction $\lambda x{:}A.\,t$ has type $A\to B$ whenever $t$ has type $B$ in the context extended with $x:A$ ; and application $f\,u$ has type $B$ whenever $f:A\to B$ and $u:A$ .

\dfrac{\Gamma, x{:}A \vdash t : B}{\Gamma \vdash \lambda x{:}A.\,t : A\to B} \qquad \dfrac{\Gamma \vdash f : A\to B \quad \Gamma \vdash u : A}{\Gamma \vdash f\,u : B}

Martin-Löf dependent type theory generalizes this further: the result type of a function can depend on the value of its argument. The ** $\Pi$ -type** (dependent function type) $\prod_{x:A} B(x)$ collects functions sending each $x:A$ to a term of type $B(x)$ — when $B$ doesn't mention $x$ , this collapses to the ordinary $A\to B$ . Dually, the ** $\Sigma$ -type** (dependent pair type) $\sum_{x:A} B(x)$ collects pairs $\langle a,b\rangle$ with $a:A$ and $b:B(a)$ — a pair whose second component's type depends on the first; when $B$ doesn't mention $x$ , this collapses to the ordinary product $A\times B$ .

\prod_{x:A} B(x), \qquad \sum_{x:A} B(x)

Dependent types and their Curry–Howard reading
Type constructor	Non-dependent special case	Curry–Howard reading
$\prod_{x:A} B(x)$	$A\to B$ (when $B$ is constant)	$\forall x{:}A,\ B(x)$
$\sum_{x:A} B(x)$	$A\times B$ (when $B$ is constant)	$\exists x{:}A,\ B(x)$
Univalence: $(A\simeq B) \simeq (A =_{\mathcal U} B)$	—	Equivalent types are identified

Theorem: Strong normalization for simply typed lambda calculus

If $\Gamma \vdash t : A$ in the simply typed lambda calculus, then $t$ is strongly normalizing: every sequence of $\beta$ -reductions starting from $t$ terminates after finitely many steps.

Why is it true?

This is why simply typed lambda calculus, despite having function application and recursion-like nesting, is not Turing-complete — no well-typed term can loop forever, which is exactly what makes type-checkers in this fragment always terminate.

Proof

(Tait's reducibility method.) Define, by induction on the structure of types, a set $\mathrm{RED}_A$ of "reducible terms" for every type $A$ : for a base type $o$ , let $\mathrm{RED}_o$ be the set $SN$ of all strongly normalizing terms; for a function type, let $\mathrm{RED}_{A\to B} = \{t : \text{for every } u \in \mathrm{RED}_A,\ t\,u \in \mathrm{RED}_B\}$ .

One first proves, by induction on $A$ , three technical properties together: (CR1) every term in $\mathrm{RED}_A$ is strongly normalizing; (CR2) $\mathrm{RED}_A$ is closed under $\beta$ -reduction (if $t\in\mathrm{RED}_A$ and $t\to t'$ then $t'\in\mathrm{RED}_A$ ); (CR3) any "neutral" term (a variable or application, not an abstraction) all of whose one-step reducts already lie in $\mathrm{RED}_A$ must itself lie in $\mathrm{RED}_A$ . The base case is immediate from the definition of $SN$ ; the function-type case unfolds the definition of $\mathrm{RED}_{A\to B}$ and uses the induction hypothesis on the smaller types $A$ and $B$ .

Next, one shows every well-typed term is reducible under any substitution of reducible terms for its free variables: by induction on the typing derivation of $\Gamma \vdash t:A$ , if $\sigma$ assigns each variable $x$ in $\Gamma$ a term $\sigma(x)\in\mathrm{RED}_{\Gamma(x)}$ , then $t\sigma \in \mathrm{RED}_A$ . The variable case is immediate. The application case follows directly from the definition of $\mathrm{RED}_{A\to B}$ . The abstraction case needs the most care: for $(\lambda x.\,t)\sigma$ applied to any $u\in\mathrm{RED}_A$ , the term reduces in one $\beta$ -step to $t(\sigma,x{:=}u)$ , which is in $\mathrm{RED}_B$ by the induction hypothesis (applied to the extended substitution); property (CR3) — closure under "expansion" for terms whose reducts are all already reducible — then places $(\lambda x.\,t)\sigma\,u$ itself in $\mathrm{RED}_B$ , so $(\lambda x.\,t)\sigma \in \mathrm{RED}_{A\to B}$ by definition.

Finally, apply this to the identity substitution: every variable $x{:}A$ is itself neutral with no reducts at all, so it is vacuously in $\mathrm{RED}_A$ by (CR3). So for any closed derivation $\Gamma \vdash t:A$ , taking $\sigma$ to map each $x$ to itself gives $t = t\sigma \in \mathrm{RED}_A$ . By (CR1), $\mathrm{RED}_A \subseteq SN$ , so $t \in SN$ : every well-typed term is strongly normalizing. $\blacksquare$

AdvancedThe Curry–Howard correspondence

Read $A\to B$ as "if $A$ then $B$ ", read $A\times B$ as " $A$ and $B$ ", and a proof of a proposition becomes a well-typed program of the matching type — this is propositions-as-types, proofs-as-programs. Checking a proof reduces to type-checking a term; constructing a proof reduces to writing a program of the right type.

Theorem: Curry–Howard correspondence

Let $\varphi$ be a propositional formula built from atoms, $\wedge$ , and $\to$ , and let $A_\varphi$ be the simple type obtained by translating atoms to base types, $\wedge$ to product $\times$ , and $\to$ to function type $\to$ . Then $\varphi$ is provable in intuitionistic propositional logic if and only if $A_\varphi$ is inhabited: there is a closed term $t$ with $\vdash t : A_\varphi$ .

Why is it true?

This is the precise statement behind "a proof assistant is just a type-checker": Coq, Agda, and Lean accept a machine-checked proof of a theorem exactly when they accept a term of the corresponding type, and type-checking (unlike theorem-proving in general) is a small, fast, mechanical, and highly trustworthy algorithm.

Proof

(Proofs become programs.) By induction on a natural-deduction derivation of $\vdash \varphi$ . If the last rule is $\to$ -introduction, deriving $\varphi=\psi\to\chi$ from a subproof of $\chi$ under hypothesis $\psi$ : by the induction hypothesis that subproof translates to a term $t$ with $x{:}A_\psi \vdash t : A_\chi$ (the hypothesis becomes a free variable $x$ ); then $\lambda x{:}A_\psi.\,t$ is closed and has type $A_\psi\to A_\chi=A_\varphi$ . If the last rule is $\to$ -elimination (modus ponens) from $\psi\to\chi$ and $\psi$ : by the induction hypothesis we have terms $t_1 : A_\psi\to A_\chi$ and $t_2 : A_\psi$ ; then $t_1\,t_2 : A_\chi$ . The $\wedge$ -introduction and $\wedge$ -elimination rules translate symmetrically to pairing $\langle t_1,t_2\rangle$ and the two projections. Every rule of the proof system has a matching term-building rule, so induction on the derivation produces a well-typed closed term of type $A_\varphi$ .

(Programs become proofs.) Conversely, by induction on a typing derivation $\vdash t : A$ . Each typing rule — variable, abstraction, application, pairing, projection — has exactly the same tree shape as a natural-deduction rule — hypothesis, $\to$ -introduction, $\to$ -elimination, $\wedge$ -introduction, $\wedge$ -elimination. So take the same derivation tree, erase all the terms, and read each type as the formula it translates from: this is precisely a valid intuitionistic proof of $\varphi$ (where $A=A_\varphi$ ).

Since the two translations (proof $\to$ term, and term $\to$ proof) are structural inverses of each other on derivation trees — each one undoes exactly what the other does, rule by rule — $\varphi$ is provable exactly when $A_\varphi$ is inhabited. $\blacksquare$

UndergraduateReal-World Applications and Worked Examples

Rich type systems catch entire classes of bugs before a program ever runs: Rust's ownership types prevent use-after-free and data races at compile time, and dependently typed languages can encode invariants like "this list has exactly $n$ elements" or "this index is within bounds" directly into types, making certain runtime errors unrepresentable. The deepest application is inside proof assistants themselves: Coq, Agda, and Lean have small, carefully audited kernels that do nothing but type-check terms — because of the Curry–Howard correspondence, accepting a term of a theorem's type is accepting a machine-checked proof, so trusting a mathematical result the size of the Feit–Thompson theorem or the four-color theorem reduces to trusting a few hundred lines of type-checking code, not the (much larger, much harder to audit) tactics that built the proof term.

Example: A $\Pi$ -type that ordinary function types cannot express

Let $\mathrm{Vec}\,A\,n$ be the type of length- $n$ lists of elements of type $A$ . Write down a term inhabiting $\prod_{n:\mathbb N} (\mathrm{Vec}\,A\,n \to \mathrm{Vec}\,A\,n)$ — "for every length $n$ , a function on length- $n$ vectors" — and explain why simple types (without $\Pi$ ) cannot express this specification at all.

Solution

The term $\lambda n{:}\mathbb N.\,\lambda v{:}\mathrm{Vec}\,A\,n.\,v$ works: for each natural number $n$ , it takes a length- $n$ vector $v$ and returns it unchanged — plainly well-typed, since $v : \mathrm{Vec}\,A\,n$ is returned at type $\mathrm{Vec}\,A\,n$ , for whichever $n$ was supplied.

What makes this a genuine use of $\Pi$ rather than an ordinary function type is that the type of the second argument ( $\mathrm{Vec}\,A\,n$ ) mentions the value of the first argument ( $n$ ). In simply typed lambda calculus, a function's argument and result types are fixed once and for all — $A\to B$ with $A,B$ chosen before any value of type $A$ is known. There is no way to write "give me a natural number $n$ , and depending on which number you gave me, I will demand a vector of that exact length" using only $\to$ : you would need a single fixed type $\mathrm{Vec}\,A\,n$ that somehow works for every $n$ simultaneously, which is not what $\mathrm{Vec}$ means.

Concretely, if you tried to write this using ordinary function types, you could at best get $\mathbb N \to (\mathrm{Vec}\,A\,? \to \mathrm{Vec}\,A\,?)$ for one FIXED placeholder length — useless, since it would reject vectors of any other length, or accept vectors of the wrong length. The $\Pi$ -type $\prod_{n:\mathbb N}(\cdots)$ is precisely the type constructor that lets the codomain "look back" at the specific value of $n$ received, which is exactly the dependency simple types cannot express.

Example: Curry–Howard for function composition

The formula $(A\to B)\to((B\to C)\to(A\to C))$ expresses transitivity of implication. Under Curry–Howard, find the $\lambda$ -term that proves it, and verify its type derivation step by step.

Solution

The term is $t = \lambda f{:}A\to B.\,\lambda g{:}B\to C.\,\lambda x{:}A.\,g\,(f\,x)$ — exactly function composition $g\circ f$ applied to $x$ .

Derive the type from the inside out. In context $f{:}A\to B,\,g{:}B\to C,\,x{:}A$ : since $f:A\to B$ and $x:A$ , application gives $f\,x:B$ . Since $g:B\to C$ and $f\,x:B$ , application gives $g\,(f\,x):C$ .

Now discharge the abstractions from the inside out. $\lambda x{:}A.\,g\,(f\,x)$ has type $A\to C$ in context $f{:}A\to B,\,g{:}B\to C$ . Then $\lambda g{:}B\to C.\,(\cdots)$ has type $(B\to C)\to(A\to C)$ in context $f{:}A\to B$ . Finally $\lambda f{:}A\to B.\,(\cdots)$ has type $(A\to B)\to((B\to C)\to(A\to C))$ with no remaining free assumptions — a closed term.

So $\vdash t : (A\to B)\to((B\to C)\to(A\to C))$ , meaning $t$ is a Curry–Howard proof of transitivity: "if $A$ implies $B$ , and $B$ implies $C$ , then $A$ implies $C$ " — the same term that a functional programmer would write to compose two functions.

Common mistake. Do not confuse

\Pi_{x:A}B(x)

and

\Sigma_{x:A}B(x)

with mere quantifiers bolted onto an already-existing universe of sets — they are new type-forming operations, and their non-dependent special cases (

\Pi\to

ordinary function type,

\Sigma\to

ordinary product) are exactly what should make you suspicious if a "dependent type" argument never actually uses the dependency. A second common confusion: the Univalence Axiom

(A\simeq B)\simeq(A=_{\mathcal U}B)

is about propositional equality

=_{\mathcal U}

of types (a path/identification that can itself be computed with), not the much stricter definitional (judgmental) equality that the type-checker uses automatically — univalence needs to be invoked, it does not come for free from the typing rules alone.

Historical note

Alonzo Church introduced simple types in 1940 to avoid the paradoxes of untyped lambda calculus. Kurt Gödel's 1958 "Dialectica interpretation" used a typed calculus of primitive recursive functionals — a direct ancestor of typed proof interpretations — to give a constructive consistency proof for arithmetic. In 1972, Per Martin-Löf published his dependent type theory, unifying logic and computation with $\Pi$ - and $\Sigma$ -types. The observation that typed programs and logical proofs are the same objects is usually credited to Haskell Curry (1958) and William Howard (written 1969, published 1980), giving the correspondence its name. In 2013, the "HoTT Book" by the Univalent Foundations Program, following Vladimir Voevodsky's Univalence Axiom, proposed Homotopy Type Theory as a new candidate foundation for mathematics.

Kurt Gödel

ResearchResearch today

Research frontier as of 2026

Homotopy Type Theory and Voevodsky's Univalent Foundations program continue to be developed as a candidate foundation for mathematics alongside (not yet replacing) ZFC set theory, with cubical type theory (from roughly 2015 onward) giving the Univalence Axiom genuine computational content — a long-standing open problem — by building equality of types directly out of an interval type, and this computational account is still being refined and extended to richer type formers as of 2026. Large-scale formalization efforts are demonstrating type theory's power as working mathematical infrastructure: the Lean-based `mathlib` library has grown into one of the largest bodies of formalized mathematics, Peter Scholze and Dustin Clausen's 2020–2022 "Liquid Tensor Experiment" formally verified a hard theorem in condensed mathematics using Lean, and community efforts (including one led by Kevin Buzzard) toward a full formalization of Fermat's Last Theorem remain active as of the mid-2020s. Separately, research continues on higher inductive types and synthetic homotopy theory (computing homotopy groups of spheres directly inside type theory) and on strengthening dependent type theories to support more of ordinary mathematical practice without sacrificing decidable type-checking.

In simply typed lambda calculus, if $f : A \to B$ and $a : A$ , what is the type of $f\,a$ ?

Why can a proof assistant like Coq, Agda, or Lean trust a machine-checked proof thousands of lines long?

When $B(x)$ does not actually depend on $x$ , what does $\prod_{x:A} B(x)$ reduce to?

The Univalence Axiom $(A\simeq B) \simeq (A =_{\mathcal U} B)$ says that...

References

The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics
Wikipedia contributors (2024). Curry–Howard correspondence
Wikipedia contributors (2024). Intuitionistic type theory