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 on-line via canvas, the TUE education environment 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

This schedule may be subject to changes!


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 chosse 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: Thursday April 8; 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