IMC010: Type Theory and Rocq

Teachers

Freek Wiedijk, freek@cs.ru.nl
Herman Geuvers, herman@cs.ru.nl
Niels van der Weide, n.vanderweide@cs.ru.nl
Simcha van Collem, simcha.vancollem@ru.nl

Structure of the course

The course consists of five parts:

1. Lectures

Freek will teach the basics of type theory from:

Femke van Raamsdonk, Logical Verification Course Notes

Herman and Niels will teach some metatheory from:

Herman Geuvers, Introduction to Type Theory

using the schedule:

3 September	introduction & lambda calculus	Freek: intro slides, with pauses
10 September	propositional logic & simple types	Freek: 1 & 2 slides, with pauses coq file
17 September	Church-Rosser property & principal types	Herman: 3.1, 4.1–4.3 slides, exercises CR + answers, exercises PT + answers
24 September	predicate logic & dependent types	Freek: 4 & 6 slides, with pauses coq file
1 October	inductive types	Freek: 3 slides, with pauses coq file
8 October	second-order logic & polymorphic types	Freek: 7 & 8 slides, with pauses coq file
15 October	normalization for λ→ and λ2	Niels: 4.4, 5.6 slides, exercises + answers

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

zip file with the practicum files

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 October

two 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

list of possible projects

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

Presentation 1:
Section 2.5 in Notes on Realizability by Andrej Bauer
Codrin Iftode + Johannes Kool

19 November

Presentation 2:
Until Lemma 2 (included) in Polymorphism is not set-theoretic by John Reynolds
DOI: 10.1007/3-540-13346-1_7
Mart Rietdijk + Martijn van de Wouw

Presentation 3:
Remainder of Polymorphism is not set-theoretic by John Reynolds
DOI: 10.1007/3-540-13346-1_7
Thijs van den Berg + Ties Steijn

26 November

Presentation 4:
Sections 2 and 3.1 in Realizability models for type theories by Bernard Reus
DOI: 10.1016/S1571-0661(04)00108-2
Marloes Steenbergen + Thijs van de Griendt

Presentation 5:
Section 4 in Realizability models for type theories by Bernard Reus
DOI: 10.1016/S1571-0661(04)00108-2
Ard van der Putten + Tom Janssen

3 December

Presentation 6:
Sections 7.1-7.2 in An extended calculus of constructions by Zhaohui Luo
Justin Kasteleijn + Teun van Brakel

Presentation 7:
Sections 7.3-7.4 in An extended calculus of constructions by Zhaohui Luo
Floris Reuvers + Leonne Snel

5 December

Presentation 8:
Sections 1-2 in Extracting Fω's Programs from Proofs in the Calculus of Constructions by Christine Paulin-Mohring
DOI: 10.1145/75277.75285
Ivo Nabuurs + Ruben van de Sande

Presentation 9:
Sections 3 in Extracting Fω's Programs from Proofs in the Calculus of Constructions by Christine Paulin-Mohring
DOI: 10.1145/75277.75285
Ben van Wijngaarden + Sem Stammen

10 December

Presentation 10:
Sections 1-3 in Induction is not derivable in second order dependent type theory by Herman Geuvers
DOI: 10.1007/3-540-45413-6_16
Hilde Ottens + Sonia

Presentation 11:
Section 4 in Induction is not derivable in second order dependent type theory by Herman Geuvers
DOI: 10.1007/3-540-45413-6_16
Josja Koopmans + Matej Hora

12 December

Presentation 12:
Section 2 in A logic for parametric polymorphism by Gordon Plotkin and Martin Abadi
DOI: 10.1007/BFB0037118
Supplementary material: Notes on the Abadi-Plotkin logic for parametricity by Dan Frumin
Arvid Bonten + Axel van Abkoude

17 December

Presentation 13:
Sections 2, 3.1, 3.2 in Realizability and parametricity in pure type systems by Jean-Philippe Bernardy and Marc Lasson
DOI: 10.1007/978-3-642-19805-2_8
Eskil Dam + Sophie Krijgsman

Presentation 14:
Sections 3.3, 3.4, 4 in Realizability and parametricity in pure type systems by Jean-Philippe Bernardy and Marc Lasson
DOI: 10.1007/978-3-642-19805-2_8
Erin Leachman + Kati Overbeeke

So, summarizing, the schedule for the presentations is:

12 November	presentation 1	Codrin Iftode + Johannes Kool
19 November	presentation 2	Mart Rietdijk + Martijn van de Wouw
	presentation 3	Thijs van den Berg + Ties Steijn
26 November	presentation 4	Marloes Steenbergen + Thijs van de Griendt
	presentation 5	Ard van der Putten + Tom Janssen
3 December	presentation 6	Justin Kasteleijn + Teun van Brakel
	presentation 7	Floris Reuvers + Leonne Snel
5 December	presentation 8	Ivo Nabuurs + Ruben van de Sande
	presentation 9	Ben van Wijngaarden + Sem Stammen
10 December	presentation 10	Hilde Ottens + Sonia
	presentation 11	Josja Koopmans + Matej Hora
12 December	presentation 12	Arvid Bonten + Axel van Abkoude
17 December	presentation 13	Eskil Dam + Sophie Krijgsman
	presentation 14	Erin Leachman + Kati Overbeeke
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.