IMC010: Type Theory and Rocq

Teachers

Structure of the course

The course consists of five parts:

1. Lectures

Freek will teach the basics of type theory from:

Herman and Niels will teach some metatheory from:

using the schedule:

3 Septemberintroduction & lambda calculusFreek: intro
slides, with pauses
10 Septemberpropositional logic & simple typesFreek: 1 & 2
slides, with pauses
coq file
17 SeptemberChurch-Rosser property & principal typesHerman: 3.1, 4.1–4.3
slides
24 Septemberpredicate logic & dependent typesFreek: 4 & 6
slides, with pauses
coq file
1 Octoberinductive typesFreek: 3
slides, with pauses
coq file
8 Octobersecond-order logic & polymorphic typesFreek: 7 & 8
15 Octobernormalization for λ→ and λ2Niels: 4.4, 5.6

2. Rocq practicum

There will be a Rocq practicum corresponding to Femke's course notes. For this you need to install Rocq 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.

This is the first half of the course.

3. 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, Niels and Herman, and not the topic of the reading group.

The date of the exam will be:

24 Octobertwo 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.

4. Rocq project

Each student has to do a small Rocq 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 Rocq project is 21 December 2025.

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 the semantics of the Calculus of Constructions.

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.

To motivate everyone to participate in the reading group to the end, there will be a 45 minute test about the subject of the presentations on the final Friday, which for 10% will count as a bonus to the presentation mark.

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

12 November

19 November

26 November

3 December

5 December

10 December

12 December

17 December

So, summarizing, the schedule for the presentations is:

12 Novemberpresentation 1Codrin Iftode +
Johannes Kool
19 Novemberpresentation 2Mart Rietdijk +
Martijn van de Wouw
presentation 3Thijs van den Berg +
Ties Steijn
26 Novemberpresentation 4Marloes Steenbergen +
Thijs van de Griendt
presentation 5Ard van der Putten +
Tom Janssen
3 Decemberpresentation 6Justin Kasteleijn +
Teun van Brakel
presentation 7Floris Reuvers +
Leonne Snel
5 Decemberpresentation 8Ivo Nabuurs +
Ruben van de Sande
presentation 9Ben van Wijngaarden +
Sem Stammen
10 Decemberpresentation 10Hilde Ottens +
Sonia Welinder
presentation 11Annika Heskamp +
Eskil Dam
12 Decemberpresentation 12Arvid Bonten +
Axel van Abkoude
presentation 13Jens Reinders +
Josja Koopmans
17 Decemberpresentation 14Matej Hora +
Sophie Krijgsman
presentation 15Erin Leachman +
Kati Overbeek
19 December
(second hour)		bonus test about the presentations

Grading

You will get three marks: for the exam, for the Rocq project, and for the Rocq presentations (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