Strong Normalization for the Calculus of Constructions

TL;DR

This paper reviews three proofs of the strong normalization property of the calculus of constructions, a foundational system for dependently typed programming languages like Coq and Agda, emphasizing their structural similarities and differences.

Contribution

It provides a comparative analysis of three different proofs of strong normalization for the calculus of constructions, clarifying their methodologies and motivations.

Findings

All three proofs establish strong normalization for CC.

The proofs share structural similarities despite different approaches.

Differences are driven by varying proof goals and techniques.

Abstract

The calculus of constructions (CC) is a core theory for dependently typed programming and higher-order constructive logic. Originally introduced in Coquand's 1985 thesis, CC has inspired 25 years of research in programming languages and type theory. Today, extensions of CC form the basis of languages like Coq and Agda. This survey reviews three proofs of CC's strong normalization property (the fact that there are no infinite reduction sequences from well-typed expressions). It highlights the similarities in the structure of the proofs while showing how their differences are motivated by the varying goals of their authors.