Course Materials

Topics

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.

-- WouterSwierstra - 22 Feb 2013