The course will cover three topics:
- a general introduction to dependent types and their implementation;
- the Coq proof assistant;
- the Agda programming language.
In addition to regular homework assignments, students will be expected to present a research paper related to dependently typed programming. Furthermore, students will also need to work on a larger verification project in Coq.
- 22 Feb 2013