- Bernard van Gastel
- Jeroen Claasens
- Bas van Dijk
- Roel van Dijk

We use the course by Femke van Raamsdonk of the Free University Amsterdam:

- The course notes
- Old slides from 2004:

- The practical work in Coq
- The practical work on paper, part one
- The practical work on paper, part two

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 exercise paper (and its postscript original)

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

**23 January 2008**

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.