IMC010: Type Theory and Coq


Structure of the course

The course consists of six parts:

1. Lectures on the type theory of Coq

Freek will use the first five weeks to teach part of:

using the schedule:

8 Septemberintroduction & lambda calculusslides, with pauses
15 Septemberpropositional logic & simple typeschapters 1 & 2
slides, with pauses
coq file
22 Septemberpredicate logic & dependent typeschapters 4 & 6
slides, with pauses
coq file
29 Septemberinductive typeschapter 3
slides, with pauses
coq file
6 Octobersecond-order logic & polymorphic typeschapters 7 & 8
slides, with pauses
coq file

2. Coq practicum

There will be a Coq practicum corresponding to Femke's course notes. For this you need to install Coq and download a

The completed files need to be handed in in Brightspace. Finishing this practicum is obligatory to be able to pass the course, but there will not be a grade for it.

3. Lectures on metatheory

Then Herman will use the next three weeks to teach part of:

using the schedule:

13 Octoberprincipal types & type checkingsections 4.1-4.3, 6.4
slides, exercises, answers
20 OctoberChurch-Rosser propertysection 3.1
slides, exercises, answers
10 Novembernormalization of λ→ and λ2sections 4.4, 5.6
slides, exercises, answers

This concludes the first half of the course.

4. Exam

The exam will not be at the end of the course but halfway through. Therefore the subject of the exam will be just the lectures by Freek and Herman, and not the topic of the reading group.

The dates of the exam will be:

17 November
16 January
three hour exam on the theory 

See at the end of this web page for some material to practise for the exam, like old exams from last years.

5. Reading group with presentations

In the second half of the course we read papers about a specific topic related to a recent research publication (a different topic every year). The topic of this year will be be logical relations.

The presentations are by the students in pairs. These presentations are 45 minutes, and should contain both examples, as well as the gist of the proofs in the paper. It is more important to explain the important points of the paper well, then to cover everything in full detail.

The reading material for this year, together with the students that will present them, are:

So the schedule for the presentations is:

24 NovemberTermination of STLCJoos Munneke +
Robert Kunst
Safety of STLCMaud van de Lockant +
Susan Withaar
slides pptx
27 NovemberSafety of STLC + μLucas van Kasteren +
Rico te Wechel
Safety of STLC + μ, "semantic approach"Cleo Gerards +
Dick Blankvoort
1 DecemberSemantics/typing of referencesJorrit de Boer +
Sipho Kemkes
Semantics/typing of existential typesQuinten Kock +
Sijmen van Bommel
slides pptx
4 DecemberSafety of STLC + immutable referencesPatrick van Beurden +
Razvan Potcoveanu
Safety of mutref + ∀/∃ problem + intuitive solutionDmitrii Mikhailovskii +
Marijn van Wezel
8 DecemberSafety of mutref + ∀/∃, definitionsSergio Domínguez
Parametricity λ2David Logtenberg +
Thomas van Bavel
11 DecemberParametricity λ2Alex van Tilburg +
Billy Price
15 DecemberBinary logrel for mutref + ∀/∃ + μ, Factor step-indexing with ▹ modalityCas Haaijman +
Ioannis Koutsidis
Data abstraction + logical relations in IrisLean Ermantraut +
Menzo van Kessel

6. Coq project

Each student has to do a small Coq project. This project can be chosen from

but if students have a suggestion for an interesting project that they want to do, that is also allowed.

The deadline for the Coq project is 20 January 2024.


You will get three marks: for the exam, the Coq presentations, and the Coq project (items 4, 5 and 6 above). The final mark for the course is the average of those three marks, rounded to a half integral number. A mark of 5.5 will be rounded up to 6, and the mark for the exam has to be at least 5.0.

Some supporting material

Supporting documents

Paper exercises

Old exams