paper

Propositions as Types

  • Authors:
Read the paper

đź“ś Abstract

The correspondence between propositions and types is a deep discovery that informs the design of programming languages and logic. This paper surveys the many forms of propositions-as-types, tracing the idea from its roots in the work of Brouwer, Kolmogorov, and Heyting, through the discovery of the Curry-Howard correspondence, to the present day. Along the way we encounter connections to logic programming, domain theory, category theory, and homotopy theory. The journey takes us from intuitional logic to intercalation calculus to dependent types and beyond. By viewing propositions as types we acquire a unity of logic and computation.

✨ Summary

The paper “Propositions as Types” by Philip Wadler, published in August 2015, explores the deep and influential correspondence between propositions and types, tracing its historical and theoretical development. This powerful idea has become central to the design and analysis of programming languages and logical systems. Wadler’s exposition revisits the work of pioneers like Brouwer, Kolmogorov, and Heyting, and leads up to the Curry-Howard correspondence, which fundamentally links logic to computational concepts. The paper discusses various domains where propositions-as-types play a role, such as logic programming, domain theory, category theory, and homotopy theory, emphasizing their impact on programming languages and formal systems.

This paper had a significant reach and is often cited in discussions about type theory and its applications. Notably, it aids in the development and understanding of modern type systems employed in functional programming languages such as Haskell, OCaml, and others, which utilize advanced type concepts inspired by this correspondence.

Relevant citations include:

  1. “The Curry-Howard Isomorphism” - https://www.cambridge.org/core/books/curryhoward-isomorphism/0BC9B42B0C3B6EA2E70C588E19575EC3
  2. “Propositions as Types (Curry-Howard Correspondence)” - https://plato.stanford.edu/entries/type-theory/
  3. “Logical Foundations of Mathematics and Computational Complexity: A Gentle Introduction” - https://www.springer.com/gp/book/9783319113575
  4. “Certified Programming with Dependent Types” - https://mitpress.mit.edu/9780262528900/certified-programming-with-dependent-types/