Sign In

Communications of the ACM

Contributed articles

Propositions as Types

Propositions as Types, illustration


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.

Back to Top

Key Insights


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.


CACM Administrator

The following letter was published in the Letters to the Editor of the March 2016 CACM (
--CACM Administrator

Contrary to what Philip Wadler suggested in his otherwise interesting and informative article "Propositions as Types" (Dec. 2015, page 76, middle column, third paragraph), the algorithmic decidability of an axiomatically defined theory, say, T (such as Set Theory, as in Hilbert's concern) does not presuppose the negation- or "Gdel-" completeness (not to be confused with the semantic completeness) of T. First, negation-completeness does not imply algorithmic decidability without further ado, and second, negation-incompleteness does not imply algorithmic undecidability. The negation-completeness of T does indeed imply the algorithmic decidability of T if the set of axioms of T is algorithmically decidable and T is consistent (recall Recursion Theory), and there are theories that are negation-incomplete but algorithmically decidable (such as temporal-logical theories), respectively.(1)

Simon Kramer
Lausanne, Switzerland

(1) Kramer, S. Logic of negation-complete interactive proofs (formal theory of epistemic deciders). Electronic Notes in Theoretical Computer Science 300, 21 (Jan. 2014), 4770, section 1.1.1.


Thank you to Simon Kramer for clarifying the relation between completeness and decidability. The word "presupposes" has two meanings: "require as a precondition of possibility or coherence" and "tacitly assume at the beginning of a line of argument or course of action that something is the case." Kramer presupposes I mean the former, when in fact I mean the latter; my apologies for any confusion. The logics in question are consistent and have algorithmically decidable axioms and inference rules, so completeness indeed implies decidability.

Philip Wadler
Edinburgh, Scotland

Displaying 1 comment

Log in to Read the Full Article

Sign In

Sign in using your ACM Web Account username and password to access premium content if you are an ACM member, Communications subscriber or Digital Library subscriber.

Need Access?

Please select one of the options below for access to premium content and features.

Create a Web Account

If you are already an ACM member, Communications subscriber, or Digital Library subscriber, please set up a web account to access premium content on this site.

Join the ACM

Become a member to take full advantage of ACM's outstanding computing information resources, networking opportunities, and other benefits.

Subscribe to Communications of the ACM Magazine

Get full access to 50+ years of CACM content and receive the print version of the magazine monthly.

Purchase the Article

Non-members can purchase this article or a copy of the magazine in which it appears.