---
title: "Programming in Martin-Löf's Type Theory: An Introduction"
authors:
  - "Bengt Nordström"
  - "Kent Petersson"
  - "Jan M. Smith"
year: 1990
venue: "Oxford University Press"
arxiv: null
doi: null
source: "https://www.cse.chalmers.se/research/group/logic/book/"
topics:
  - martin-lof
  - type-theory
  - dependent-types
  - textbook
seed_rank: 653
seed_batch: "perfects-pl-2026-08-13"
reviewed: "2026-08-13"
pool: "languages"
relevance_score: 10
lineage: programming-language-foundations
cites:
  - title: "An Intuitionistic Theory of Types: Predicative Part"
    url: "https://doi.org/10.1016/S0049-237X(08)71945-1"
    year: 1975
    arxiv: null
    doi: "10.1016/S0049-237X(08)71945-1"
  - title: "Constructive Mathematics and Computer Programming"
    url: "https://doi.org/10.1016/S0049-237X(09)70189-2"
    year: 1982
    arxiv: null
    doi: "10.1016/S0049-237X(09)70189-2"
  - title: "The Formulae-as-Types Notion of Construction"
    url: "https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf"
    year: 1980
    arxiv: null
    doi: null
  - title: "Implementing Mathematics with the Nuprl Proof Development System"
    url: "https://nuprl-web.cs.cornell.edu/book/"
    year: 1986
    arxiv: null
    doi: null
see:
  - "648-an-intuitionistic-theory-of-types-predicative-part"
  - "649-constructive-mathematics-and-computer-programming"
  - "647-the-formulae-as-types-notion-of-construction"
  - "654-implementing-mathematics-with-nuprl"
---

# Programming in Martin-Löf's Type Theory: An Introduction

## One-sentence takeaway

Nordström, Petersson, and Smith turn Martin-Löf's judgmental type theory into a programmer's book: sets, propositions, and inductive families are the constructs you write, not just the rules you cite.

## Why it matters here

Ano's sized/dependent array story is closer to this MLTT presentation than to System F; the book is how you learn to program in the theory Anoptic would extract kernels from, not only how to quote it.

## Key ideas

- Four judgment forms (A set, A = B, a ∈ A, a = b ∈ A) are primitive; propositions-as-sets is a derived reading, not a slogan pasted on.
- Π, Σ, +, Id, W/well-orderings, and universes à la Martin-Löf are given with introduction, elimination, and equality rules intended for use.
- The 1990 OUP text is the standard introduction; Chalmers hosts the out-of-print edition.
- Direct ancestor of the Agda/Epigram teaching line; Nuprl is the contemporary implemented cousin, not a replacement.

## Caveats

## Links

- Chalmers edition: https://www.cse.chalmers.se/research/group/logic/book/