Proving with Computer Assistance 2IMF15


Herman Geuvers: home page
Room number MF6.079A (only on Thursdays) For contact, use the e-mail address herman at cs dot ru dot nl

Location and time

The course will be given live on


We assume that you are familiar with a bit of logic, especially natural deduction and preferably (untyped) lambda calculus.


System we will use

We will be using the Proof Assistant Coq in this course.

Some useful links

The course by week

The course will note be recorded, but recordings of the previous year are provided on Canvas. This year's course will roughly be the same schedule as last year. This schedule may be subject to changes! Especially the slides and exercises may be slightly adapted as we go along the course.


The mark for the course is determined by the 2 marks you will get for the two items listed below. For the retake exam ("Hertentamen"), all guidelines above apply with the following dates/deadlines: NB. You can choose to only retake one part of the exam, so only the Written exam, or only the Coq assignment. In any case: register for the retake!

Coq Assignments

Deadline: Wednesday April 17; do the assignment in couples deliver your assignment by mail to the teacher.

Here is a page about the of Coq assignment. (Look here for some additional comments regarding the use of lists.) To complete the Coq assignment follow these steps:

A couple of remarks concerning the report:

herman at cs dot ru dot nl