|Website:||website containing additional information|
|Period:||periode 1 (week 36 t/m 45, dwz 9-9-2010 t/m 12-11-2010; herkansing week 1)|
|Participants:||up till now 7 subscriptions|
|Schedule:||Note: from now on the schedule is to be found in Osiris|
|Teachers:||Dit is een oud rooster!
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.
|Literature:||Tutorials and research papers, available online. The exact material being discussed will be made available on the course web page.|
|Course form:||Sessions will comprise a mix of presentations by the participants or the lecturer, lively discussions, and problem-solving. Students are expected to prepare for the sessions by reading the given material, by answering specific theoretical questions or by implementing practical assignments in a dependently-typed programming language.|
|Exam form:||The final grade will be computed as follows:
|Minimum effort to qualify for 2nd chance exam:|