In this seminar we will study functional programming with dependent types. Dependent type theories have a long history of being used to formalize the foundations of mathematics and theorem proving. More recently, they have started to draw interest from the programming language community.

In many languages it is possible to define types that generalize over other types. Familiar examples from Haskell may be polymorphic lists, trees, or other parameterized algebraic data structures. A dependent type is a type that is parameterized by a value rather than another type. This gives programmers a richer language of data types, together with a wealth of new programming techniques. In this seminar we will see how dependent types subsume many topics from other programming courses, such as generic programming or program verification.

A programming language with dependent types provides a single unified framework in which you can write, execute and reason about your programs. We will study both the verification and programming practice using dependent types using modern systems such as Coq and Agda.