IMC010: Type Theory and Coq



The course will be taught using Zoom.

The Zoom address will be disseminated through Brightspace. Therefore, if you want to participate in the course, make sure that you are registered there.

Brightspace also will contain videos for the course, and it will be used to send email and keep track of results.

Structure of the course

The course consists of six elements:

1. Lectures about using type theory

Freek will use the first five weeks to teach:

using the schedule:

31 Augustintroduction & propositional logicchapter 1
7 Septembersimple type theory & inductive typeschapters 2 & 3
14 Septemberpredicate logic & dependent typeschapters 4 & 6
21 Septembersecond-order logic & polymorphic typeschapters 7 & 8
28 Septemberprogram extraction & inhabitationchapters 5 & 9

2. Coq practicum

There will be a

which you can do either in the ProofWeb server (using an ancient version of Coq), as well as in Coq installed on your own machine. For this here is a

Finishing this practicum is obligatory to be able to pass the course, but there will not be a grade for it. The first person to get all-green traffic lights on the Coq practicum in the ProofWeb server will win a small price.

3. Lectures on some metatheory

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

using the schedule:

5 Octoberprincipal types and type checkingsections 4.1-4.3, 6.4
slides, exercises, answers
12 OctoberChurch-Rosser propertysection 3.1
slides, exercises, answers
19 Octobernormalization of λ→ and λ2sections 4.4, 5.6
slides, exercises, answers

This concludes the first half of the course.

4. Exam

As an experiment we will have the exam not 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:

2 Novembertwo hour exam on the theory 
3-4 Novemberindividual ten minute oral exam as a follow-up

The exam will be at home without supervision and will be open book/open Coq session. Each student will get a different selection from a larger set of exercises. The answers will have to be submitted through Brightspace as a scan or digital photos.

The exam will be followed by a ten minute oral the days after.

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 a recent research paper, together with a reading list that leads up to this paper.

The topic of the paper this year will be a formal semantics for the Rust programming language, and its formalization in Coq. One of the authors of the paper is Robbert, one of the teachers of the course. The paper is too advanced to fully understand at the level of the course, but we will work on the most important elements.

The presentations are by the students in pairs (and one paper by three students). 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 7 papers that will be presented in 12 presentations are:

For help with the first six papers it is best to go to Jules, and about the last paper it is best to ask Robbert.

The presentations will be through the standard Zoom channel on Monday at 08:30 (one presentation per meeting) and on Thursday, also at 08:30 (two presentations per meeting). The schedule for the presentations is:

Mon 23 November 1: Rust Niek Janssen
+ Sander Karsten
Thu 26 November 2: Rust Rowan Goemans
+ Stefan Schrijvers
slides, files
3: Substructural Type Systems Els Hoekstra
+ Mirja van de Pol
Mon 30 November 4: Separation Logic Toine Hulshof
+ Rick van der Wal
Thu 3 December 5: Separation Logic Rob van der Drift
+ Pieter Cas Kolijn
6: Concurrency Loes Kruger
+ Michiel Verloop
Mon 7 December 7: Concurrency Justin Reniers
+ Johan Sijtsma
Thu 10 December 8: Blog post Derek Dreyer Ruben Holubek
+ Gunnar Noordbruis
9: Logical Relations Eline Bovy
+ Alex van de Griendt
+ Tosca Klijnsma
Mon 14 December 10: Logical Relations Jeroen Kool
+ Cárolos Laméris
Thu 17 December 11: RustBelt Luko van der Maas
+ Ceel Pierik
12: RustBelt Rick Koenders
+ Mees Meuwissen

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 will be exactly two weeks after the last presentation in the reading group ends.


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.


As part of the research in our group, we are developing new, experimental proof automation using Machine Learning for Coq, and we would like you to help us test it. Participation is completely voluntary. Installation and usage instructions can be found here. If you have any questions, you can send an email to, or ask a question on Discord.

Some supporting material

Paper exercises

Old exams

Some slides