![Type Theory and the Curry-Howard Correspondence](https://cdn.slatesource.com/5/4/e/54eb8920-f47b-4567-9981-a855de2b1240.jpg)

# Type Theory and the Curry-Howard Correspondence

- [Made in Slatesource](https://slatesource.com/s/1036)
- By [KaiRenner](https://slatesource.com/u/KaiRenner)
- Science & Technology
- Created on Mar 23, 2026

## The Unexpected Bridge Between Logic and Programming

The Curry-Howard correspondence, discovered independently by Haskell Curry in 1934 and William Howard in 1969, reveals that types are propositions and programs are proofs. Writing a program that type-checks is equivalent to constructing a mathematical proof. This is not a metaphor — it is a precise structural isomorphism between two independently developed formal systems.

Types as Specifications

A type signature f : Int to Bool is a claim: given an integer, this function produces a boolean. Type checking verifies this claim mechanically. But simple types are shallow specifications — they say nothing about whether the integer must be positive, or

The Simply-Typed Lambda Calculus

Adding types to the lambda calculus gives the simply-typed lambda calculus (STLC). Every term has a type, and the type system rejects terms that would get stuck — applying a number as a function, for instance. The correspondence: the type A to B correspon

Dependent Types

In dependent type theory, types can depend on values. The type Vector n a is the type of lists of length exactly n containing elements of type a. The length is part of the type. A function append : Vector m a to Vector n a to Vector (m+n) a encodes the fa

Proof Assistants and Formal Verification

Coq and Agda are proof assistants based on dependent type theory. Writing a program in Coq means constructing a proof that the program meets its specification. The seL4 microkernel — used in safety-critical embedded systems — was verified in Coq: a machin

> The seL4 verification does not mean the system is perfect. It means every security property stated in the specification is guaranteed by mathematical proof. The specification itself is a human product and may be wrong. Proof moves the uncertainty from the
>
> — KaiRenner · 24th of March 2026

Homotopy Type Theory

Homotopy Type Theory (HoTT) is a recent unification of type theory with algebraic topology. Types are interpreted as topological spaces, and proofs of equality are interpreted as paths between points. This provides a new foundation for mathematics in whic

## Go Deeper: Type Theory as a Foundation for Mathematics

Type theory is one proposed foundation for all of mathematics — an alternative to set theory. Classical mathematics is usually founded on set theory, and set theory has its own surprising paradoxes and fundamental limitations that took decades to resolve. Those limitations illuminate why foundations matter.

[

![Understand Set Theory and Gödel's Theorems](https://cdn.slatesource.com/e/6/6/e66e0e37-c5f4-4471-a3ae-5992dfe8002a.jpg)

Understand Set Theory and Gödel's TheoremsBy KaiRenner

](/s/1031)

[Homotopy Type Theory](https://homotopytypetheory.org/book/?utm_source=slatesource)