# Per Martin-Löf

> 1942– · Mathematician, Logician
>
> **Recorded contribution:** Intuitionistic type theory — foundation of modern proof assistants (Coq, Agda, Lean)

## How to use this dossier

Read for a causal chain, not a hero story: inherited problem → contribution → mechanism → downstream capability → limit. Then close the page and complete the reconstruction exercise from memory.

## 1. Historical orientation

Per Martin-Löf (born 1942) is a Swedish logician and statistician who created intuitionistic type theory. In this foundation, a proposition is understood through what counts as its proof, and a type is understood through how its values are constructed. The propositions-as-types correspondence makes a proof of an implication behave like a function and a proof of existence contain a witness. Dependent types let later types mention values, enabling specifications such as vectors indexed by length. Coq, Agda, Lean, and other proof assistants draw from this lineage, but each also incorporates Curry–Howard, de Bruijn, Girard, Coquand, Huet, and many additional traditions.

## 2. The problem inherited

Foundations separated programs from proofs, while constructive mathematics needed a precise system in which existence provides an explicit witness and computation preserves meaning.

## 3. The central contribution

Martin-Löf designed a constructive dependent type theory where proofs are checkable terms and normalization executes their computational content.

## 4. Reconstruct the mechanism

1. Represent a proposition as a type and a proof as a term inhabiting that type.
2. Use function types for implication, product types for conjunction, and dependent pairs for existential statements with witnesses.
3. Allow a type to depend on a value, so an interface can encode invariants such as a vector's length.
4. Reduce terms by computation and check them against typing rules in a small verifier.

## 5. What changed downstream

- Dependent type theory became a foundation for interactive theorem proving and verified programming.
- Proofs can extract executable programs whose types certify stated properties.
- The work connected constructive mathematics, logic, language design, and proof assistants.

## 6. Attribution, limits, and uncertainty

- The broader propositions-as-types lineage includes Brouwer, Heyting, Curry, Howard, de Bruijn, and others.
- Different versions of Martin-Löf type theory vary in universes, equality, extensionality, and consistency strength.
- A machine-checked proof depends on definitions and trusted kernels and may omit performance or environment assumptions.

## 7. Reconstruction lab

In a proof assistant, define vectors indexed by length and write append with result length m+n. Inspect which invalid program is rejected, then list the theorem prover, library, compiler, and hardware assumptions outside the type.

## 8. Evidence trail

- [Intuitionistic Type Theory](https://archive.org/details/Bibliopolis-MARTINLOFPer-IntuitionisticTypeTheory) — Bibliopolis
- [Per Martin-Löf](https://en.wikipedia.org/wiki/Per_Martin-L%C3%B6f) — Wikimedia Foundation

---

*Research checked 2026-08-09. Dates, roles, and claims about living people are historical snapshots. Linked sources remain the authority; this dossier is original instructional synthesis.*