|Website:||website met extra informatie|
|Onderwijs:||Het vak INFOMDTP wordt in 2013/2014 niet aangeboden.|
|Nota bene:||Er is geen recente vakbeschrijving beschikbaar.|
Onderstaande tekst is een oude vakbeschrijving uit collegejaar 2012/2013
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.
Tutorials and research papers, available online. The exact material being discussed will be made available on the course web page.
|Werkvorm:||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.|
|Toetsvorm:||The final grade will depend on the exercises, presentation, and a small research project.|
|Inspanningsverplichting voor aanvullende toets:||Om aan de aanvullende toets te mogen meedoen moet de oorspronkelijke uitslag minstens 4 zijn.|