Propositions as Types : An Introduction to Program Synthesis

Welcome to Papers We Love, Zurich! We have organized a series of talks about Curry-Howard correspondence -- one of the most fruitful “coincidences” in theoretical computer science.

In the first session, Dhruv Nevatia will present “Propositions as Types” by Philip Wadler. The paper is a lucid guide to the idea that propositions can be seen as types and proofs can be seen as programs. We’ll make this concrete by working in two parallel formalisms—the simply-typed lambda calculus and intuitionistic propositional logic—and watching the same structure show up on both sides!

Once the correspondence is in place, the natural next question is: how do we actually find proofs/programs? This is the type inhabitation problem: given a type (proposition), synthesize a program (proof) of that type (proof) i.e., it inhabits it; or determine that none exists. Seen this way, inhabitation is a form of program synthesis, and it is tightly connected to proof search.
We’ll look at proof search through a saturation-style lens: rather than guessing full proofs top-down, we incrementally generate and accumulate consequences and obligations, reusing derived facts, until the target proposition is proven, or its failure has been established.

Why care?

• For AI enthusiasts: it builds intuition for how “write me a correct program that does ...” can become a well-posed search problem. Turn the natural language spec into a type, then let proof search do the honest work of synthesizing a program that actually type-checks.
• For programmers and language users: Curry–Howard explains why types feel like lightweight specifications, and why “writing a term of this type” is often the same as “solving a small logical problem.”
• For logic enthusiasts: it offers a clean bridge between lambda calculi, natural deduction/sequent reasoning, and proof search/type i