Types, Constructions and Proofs:

A Workshop with Peter Milne