Propositions as Types

✨ Summary

Overview

Philip Wadler presents an introduction and historical account of the propositions-as-types principle, also known as the Curry–Howard correspondence. The central correspondence is that logical propositions map to types, proofs map to programs, and proof simplification maps to program evaluation. The paper illustrates this relationship through natural deduction and the simply typed lambda calculus: conjunction corresponds to product types, disjunction to sum types, and implication to function types.

The paper extends the discussion to dependent types, polymorphism, data abstraction, continuations, modal and temporal logics, linear logic, monads, session types, category theory, and homotopy type theory. It also explains how normalization and cut elimination provide computational interpretations of proof-theoretic processes, and surveys applications in proof assistants and verified systems, including Coq, NuPRL, F*, and certified compiler verification. The paper’s historical appendix records William Howard’s account of the development of the correspondence and its relationship to Curry, Prawitz, Tait, de Bruijn, and Martin-Löf. (homepages.inf.ed.ac.uk)

Influence

The paper functions primarily as a widely used survey and exposition rather than as the source of a new formal calculus. Its influence is reflected in later work that explicitly invokes propositions-as-types to connect executable programs with machine-checked specifications. For example, Refinement Reflection applies the principle to program verification in Liquid Haskell, using typed programs to express and check functional-correctness properties. The correspondence also remains a standard conceptual foundation for dependent type theory, proof assistants, verified compilation, and programming-language research. (arxiv.org)