2015 PropositionsAsTypes

• (Wadler, 2015) ⇒ Philip Wadler. (2015). “Propositions As Types.” In: Communications of the ACM Journal, 58(12). doi:10.1145/2699407

Subject Headings: Functional Programming, Curry–Howard Isomorphism.

Cited By

• http://scholar.google.com/scholar?q=%222015%22+Propositions+As+Types
• http://dl.acm.org/citation.cfm?id=2847579.2699407&preflayout=flat#citedby

Quotes

Abstract

Connecting mathematical logic and computation, it ensures that some aspects of programming are absolute.

Key Insights

• Propositions as Types observes a deep correspondence between logic and computation: propositions in a logic correspond to types in programming language; proofs of propositions corresponse to programs of the corresponding type; and simplification of proofs corresponds to evaluation of programs.
• Propositions as Types is broadly applicable, applying to a wide variety of logics (intuitionistic, second-order classical, linear) and of language features ([lambda calculus parametric polymorphism]], continuations, concurrency).
• Often the same ideas are discovered independently by logicians and computer scientists, demonstrating some asepects of programming language design are not arbitrary but absolute.

Introduction

Powerful insights arise from linking two fields of study previously thought separate. Examples include Descartes's coordinates, which links geometry to algebra, Planck's Quantum Theory, which links particles to waves, and Shannon's Information Theory, which links thermodynamics to communication. Such a synthesis is offered by the principle of Propositions as Types, which links logic to computation. At first sight it appears to be a simple coincidence — almost a pun — but it turns out to be remarkably robust, inspiring the design of automated proof assistants and programming languages, and continuing to influence the forefronts of computing.

Propositions as Types is a notion with many names and many origins. It is closely related to the BHK Interpretation, a view of logic developed by the intuitionists Brouwer, Heyting, and Kolmogorov in the 1930s. It is often referred to as the Curry–Howard Isomorphism, referring to a correspondence observed by Curry in 1934 and refined by Howard in 1969. Others draw attention to significant contributions from de Bruijn's Automath and Martin-Löf's Type Theory in the 1970s.

. …

References

;

	Author	volume	Date Value	title	type	journal	titleUrl	doi	note	year
2015 PropositionsAsTypes	Philip Wadler			Propositions As Types				10.1145/2699407		2015