Curry–Howard Isomorphism

As AI becomes stronger and stronger in coding and math, I feel that type theory will become vastly more popular. Code and math generated by AI need things like formal verification to check that it is hallucination free. I've been reading a bit of Egbert Rijke's introduction to homotopy type theory ⟦cite:Rij25⟧ . I find the part about Curry–Howard isomorphism/correspondence particularly interesting. Indeed, one can think of a mathematical proof as some kind of program. For this post, I will write a short exposition of these ideas.

Dependent Type Theory

Dependent type theory is a system of inference rules.

$$ \frac{\mathcal{H}_1 \quad \mathcal{H}_2 \quad \cdots \quad \mathcal{H}_n}{\mathcal C}. $$

Here each letter is a judgement.

A judgement in Martin-Löf's dependent type theory is one of the following:

$A$ is a (well-formed) type in context $\Gamma$, written $\Gamma \vdash A\ \mathrm{type}$.
$A$ and $B$ are judgmentally equal types in context $\Gamma$, written $\Gamma \vdash A \equiv B\ \mathrm{type}$.
$a$ is an element of type $A$ in context $\Gamma$, written $\Gamma \vdash a : A$.
$a$ and $b$ are judgmentally equal elements of type $A$ in context $\Gamma$, written $\Gamma \vdash a \equiv b : A$.

A context is a finite list of variable declarations

$$ x_1 : A_1,\ x_2 : A_2(x_1),\ \ldots,\ x_n : A_n(x_1, \ldots, x_{n-1}) $$

such that, for every $1 \leq i \leq n$, the type $A_i(x_1, \ldots, x_{i-1})$ is well-formed in the context of the preceding declarations:

$$ x_1 : A_1,\ \ldots,\ x_{i-1} : A_{i-1}(x_1, \ldots, x_{i-2}) \vdash A_i(x_1, \ldots, x_{i-1})\ \mathrm{type}. $$

Let $A$ be a type in context $\Gamma$. A family of types $B$ over $A$ in context $\Gamma$ is a type $B(x)$ in context $\Gamma, x : A$; that is,

$$ \Gamma, x : A \vdash B(x)\ \mathrm{type}. $$

Equivalently, $B(x)$ is a type indexed by $x : A$ in context $\Gamma$. Let $B$ be a family of types over $A$ in context $\Gamma$. A section of $B$ over $A$ in context $\Gamma$ is an element $b(x)$ of type $B(x)$ in context $\Gamma, x : A$; that is,

$$ \Gamma, x : A \vdash b(x) : B(x). $$

Equivalently, $b(x)$ is an element of type $B(x)$ indexed by $x : A$ in context $\Gamma$.

The specific inferences can be found in Rijke. Specifically there are dependent rules such as:

The dependent product introduction rule:
$$ \frac{\Gamma, x : A \vdash b(x) : B(x)}{\Gamma \vdash \lambda x.\, b(x) : \prod_{(x : A)} B(x)}\;\lambda. $$
The dependent sum introduction rule:
$$ \frac{\Gamma \vdash a : A \quad \Gamma \vdash b : B(a)}{\Gamma \vdash (a,b) : \sum_{(x : A)} B(x)}. $$

Identity Types

For $a,b:A$, we want $a=b$ to be a type and its elements thought of as identifications of them, defined via inductive types.

Let $A$ be a type and let $a : A$. The identity type of $a$ is the inductive family of types $a =_A x$, indexed by $x : A$, generated by the constructor

$$ \operatorname{refl}_a : a =_A a. $$

Thus, for $a,b : A$, the type $a =_A b$ (also written $\operatorname{Id}_A(a,b)$) is the type of identifications of $a$ with $b$.

The identity type is specified by the following rules:

The formation rule:
$$ \frac{\Gamma \vdash a : A}{\Gamma, x : A \vdash a =_A x\ \mathrm{type}}. $$
Once $a$ is an element of $A$, we may form, for every $x : A$, the type of identifications from $a$ to $x$.
The introduction rule:
$$ \frac{\Gamma \vdash a : A}{\Gamma \vdash \operatorname{refl}_a : a =_A a}. $$
Every element is identified with itself, by its reflexivity identification $\operatorname{refl}_a$.
The elimination rule, also called identity elimination or path induction: if $C(x,p)$ is a type in context $\Gamma, x : A, p : a =_A x$, then
$$ \frac{\Gamma \vdash a : A \quad \Gamma, x : A, p : a =_A x \vdash C(x,p)\ \mathrm{type}}{\Gamma \vdash \operatorname{ind\text{-}eq}_a : C(a,\operatorname{refl}_a) \to \prod_{(x : A)} \prod_{(p : a =_A x)} C(x,p)}. $$
To define something for every identification $p : a =_A x$, it is enough to define it for the reflexivity identification $\operatorname{refl}_a$.
The computation rule:
$$ \frac{\Gamma \vdash a : A \quad \Gamma, x : A, p : a =_A x \vdash C(x,p)\ \mathrm{type}}{\Gamma, c : C(a,\operatorname{refl}_a) \vdash \operatorname{ind\text{-}eq}_a(c,a,\operatorname{refl}_a) \equiv c : C(a,\operatorname{refl}_a)}. $$
When path induction is applied to reflexivity, it computes to the value $c$ with which the construction began.

Curry–Howard Isomorphism

The Curry–Howard correspondence reads propositions as types and proofs as elements of those types. Thus, to prove a proposition $P$ is to construct a term $p : P$; a proof can be viewed as a program, and its proposition as the program's specification.

$$ \begin{array}{c c} \text{Logic} & \text{Type theory} \\ \hline \text{propositions} & \text{types} \\ \text{proofs} & \text{elements} \\ \text{predicates} & \text{type families} \\ \top & 1 \\ \bot & \varnothing \\ P \lor Q & P + Q \\ P \land Q & P \times Q \\ P \Rightarrow Q & P \to Q \\ \neg P & P \to \varnothing \\ \exists x : A.\, P(x) & \sum_{(x : A)} P(x) \\ \forall x : A.\, P(x) & \prod_{(x : A)} P(x) \\ a = b & a =_A b \end{array} $$

References

[Rij25]Egbert Rijke. Introduction to Homotopy Type Theory. Cambridge Studies in Advanced Mathematics. Vol. 219. Cambridge University Press. 2025.