A dependent type is a type that is parameterized by a value. Simple examples are vectors of a fixed length (i.e., Vec Nat 3 to denote a vector containing exactly three natural numbers), or numbers that are restricted to a certain range (i.e, Range 3 7) to denote a natural number between 3 and 7). By mixing values with types, dependent types are extremely expressive: you can express concepts such as sorted lists, XML documents that adhere to a certain DTD or Schema, or commutative binary operators on the type level. Furthermore, dependent types allow you to express properties of your programs on the type level, and to prove them by writing programs in a programming language.

A programming language with dependent types therefore gives you a unified framework in which you can write, execute and reason about your programs.

Dependent types are a hot topic in programming language research right now, with many experimental programming languages being in development right now.

In this seminar, we will look at the theoretical foundations of programming with dependent types, and also gain practical experience by looking at concrete dependently typed programming languages and developing programs in them.

We will start with the assumption that everyone knows Haskell, and introduce dependent types systematically. For the second half of the seminar, it is possible to adjust the topics to the preferences of the participants.

• 50% theoretical and practical assignments
• 20% participation in seminar sessions
• 30% own presentation(s)