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*.

- 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).

- 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