## Proofs and Types

August – November 2016

## Administrative Details

**Evaluation**
- Assignments 30%, midsemester exam 30%, final exam 40%
- Copying is fatal

**Resources**
- Proofs and Types (Jean-Yves Girard with Paul Taylor & Yves Lafont)
- Lectures on the Curry-Howard Isomorphism (Morten Heine Sorensen & Pawel Urzyczyn)
- Derivation and Computation (Harold Simmons)

- Submit all assignments on Moodle
**only**. Further instructions will be given as part of the assignments.

## Course Plan

- Untyped lambda calculus
- (Propositional) intuitionistic logic, normalization
- Simply typed lambda calculus
- Curry-Howard isomorphism
- Classical logic and control operators
- Sequent calculus, cut elimination
- First order logic and arithmetic
- System T
- System F and second order logic
- Dependent types

## Assignments

## Lectures