Type theory reading group

General information

Course code
ITT9200
Organizer
James Chapman
ECP
3.0
What we will be reading
Syntax and Semantics of Dependent Types - Martin Hofmann
Other things you might like to read
Constructive mathematics and computer programming - Per Martin-Löf
An intuitionistic theory of types - Per Martin-Löf
Intuitionistic Type Theory - Per Martin-Löf, Bibliopolis 1984
Other things that might be useful
Agda

When and where

Meeting
Friday, 4pm -- 6pm, B101, IoC (weeks 11 -- 16)

Minutes

Friday, April 13th, 2012
Introduction and discussion of material in section 2 (James)
Friday, April 20th, 2012
Shallow embeddings in Agda (James)
Friday, April 27th, 2012
Context morphisms (James) and solution presentations (Andri, Denis)
Friday, May 4th, 2012
?

Suggested exercises