Propositions as Types

Lecturer: 
Topic: 
Logic & Computation
Level: 
Foundational
Abstract: 

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

Week: 
First week
Slot: 
11:00 - 12:30 - slot 2