Types for Programs and Proofs
The development of powerful type systems is an important aspect of modern programming language design. This course provides an introduction to this area.
In particular it introduces the notion of dependent type, a type which can depend on (is indexed by) values of another type, for example, the type of vectors indexed by its length. Dependent types are versatile.
Through the Curry-Howard identification of proposition and types virtually any property of a program can be expressed using dependent types.
The aim of the course is to give a solid and broad foundation in type systems for programming languages, and also give examples of type-based technologies in computer science.