Master class Logic 2006-2007: Type theory and Proof Assistants


This forms part of the MRI organised Master class Logic. Teachers: Herman Geuvers, [herman at cs dot ru dot nl] and Bas Spitters [spitters at cs dot ru dot nl]

Period: February 14 -- March 14 and March 28 -- May 02
Time: Wednesday 10.30 -- 13.30
Location: HG03.054 (Huygens Building, Radboud University Nijmegen). From February 21 until May 2 there will be Coq (computer) exercise classes from 11.00 to 12.00:


The relevant chapters of the two mentioned books will be handed out at the lectures.


The course consists of:

Assumed knowledge

We assume that students are familiar with the following concepts:


You have 110 minutes for your presentation. The time breakdown is as follows: List of presentations:

How to present a chapter?

You have to explain the chapter that has been assigned to you to your fellow students. You may use any kind of medium: black board, overhead projector (let us know in advance; there is no overhead projector in the room!), beamer, hand-outs. Some remarks and suggestions

Coq assignements

The following Coq formalizations have been planned. If you're name does not yet have a description behind it, please let me (Herman) know asap what you plan to do.


The students will receive a grade for each of the following three parts of the course:
  1. The presentation of their chapter
  2. The final written exam at the end: May 30, 11.00 -- 14.00, HG 03.045 (The exam will be about all the presented material.)
  3. The Coq assignment delivered at the end: Deadline Thursday June 14, send your Coq files both to Bas and Herman. (Halfway the course, each student receives an individual Coq assignment.)

Last modified: Fri May 25 18:44:20 CEST 2007