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.
-- WouterSwierstra - 22 Feb 2013