ESSLLI: Propositions as Types
Barcelona, 3—7 Aug 2015, lecturer.
The principle of Propositions as Types describes a fundamental connection
between logic and computation which views
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.
Other useful texts:
- propositions as types,
- proofs as programs, and
- normalisation of proofs as evaluation of programs.
Relation to category theory.