We use the course by Femke van Raamsdonk of the Free University Amsterdam:
The practical work in Coq for these course notes will be done on the machine prover.cs.ru.nl. Each participant will get a login to the course page on this machine. Mail Freek for a description of how to use this system (or if if you do not remember your password.)
For more practice, we will also make exercises from a paper by Henk Barendregt:
The exact selection of exercises that will be used from this paper still has to be established.
Each student will be given a small Coq formalization assignment. Assignments with a mathematical character as well as assignments with a focus on computer science will be possible. The assignment will be chosen by the student from suggestions by Freek.
The test covers both the contents of the course by Femke as well as the assignments by Henk. The test will be in the morning of
The location, time and form of the test still will have to be established.
Once every two weeks the students will have a meeting with Freek, to evaluate their progress in the course, and to help them with their understanding of the subject.
Each participant will get two grades: one for the Coq work, and one for the test. The final grade will be the average of these two grades.
The practical work of Femke's course and the exercises from Henk's paper will be corrected, but will not be graded. However, they are required work to be allowed entrance to the test.