ESSLLI: Propositions as Types

Philip Wadler

ESSLLI, Barcelona, 3—7 Aug 2015, lecturer.

The principle of Propositions as Types describes a fundamental connection between logic and computation which views

propositions as types,
proofs as programs, and
normalisation of proofs as evaluation of programs.

The course is intended to begin at the foundations and introduce students to a few intermediate or advanced topics. It is suitable for students in both logic and computing, presuming no previous knowledge of either, though familiarity with logic and computing will be helpful.

Course outline.
Propositions as Types (Slides).
The Girard-Reynolds Isomorophism (Slides).
Call-by-value is dual to call-by-name (Slides).
A taste of linear logic.
Propositions as Sessions (Slides).

Other useful texts:

Jean-Yves Girard, Paul Taylor, and Yves Lafont, Proofs and Types.
Benjamin Pierce, Types and Programming Languages.

Relation to category theory.

Claudio Hermida, Uday Reddy, Edward Robinson Logical Relations and Parametricity: A Reynolds Programme for Category Theory and Programming Languages

Philip Wadler,