|Website:||website containing additional information|
|Period:||periode 4 (week 17 t/m 27, dwz 22-4-2013 t/m 5-7-2013; herkansing week 34)|
|Participants:||up till now 12 subscriptions|
|Schedule:||Note: from now on the schedule is to be found in Osiris|
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.
|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 depend on the exercises, presentation, and a small research project.|
|Minimum effort to qualify for 2nd chance exam:||Om aan de aanvullende toets te mogen meedoen moet de oorspronkelijke uitslag minstens 4 zijn.|