IMC010: Type Theory and Coq

Teachers

Freek Wiedijk, freek@cs.ru.nl
Herman Geuvers, herman@cs.ru.nl
Niels van der Weide, n.vanderweide@cs.ru.nl
Luko van der Maas, luko.vandermaas2@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

Niels and Herman will teach some metatheory from:

Herman Geuvers, Introduction to Type Theory

using the schedule:

6 September	introduction & lambda calculus	Freek: intro slides, with pauses
13 September	propositional logic & simple types	Freek: 1 & 2 slides, with pauses coq file
20 September	Church-Rosser property & principal types	Niels: 3.1, 4.1-4.3 slides
27 September	predicate logic & dependent types	Freek: 4 & 6 slides, with pauses coq file
4 October	inductive types	Freek: 3 slides, with pauses coq file
11 October	second-order logic & polymorphic types	Freek: 7 & 8 slides, with pauses coq file
18 October	normalization for λ→ and λ2	Herman: 4.4, 5.6 slides, exercises, answers

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

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:

31 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. 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 inductive types, in particular inductive types in Martin-Löf's type theory and higher inductive types (HITs) in homotopy type theory (HoTT).

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:

Subject 1: inductive types

Per Martin-Löf, Intuitionistic Type Theory, 1980.
1. Chapter "Well-orderings"
  Rutger Broekhoff + Mikhail Ushakov: 21 November

Peter Dybjer, Inductive families, Formal Aspects of Computing 6(4), 1994.
1. Sections 1–3
  (summarized by Niels van der Weide)
2. Sections 4–6
  Niels van Duijl + Erik Oosting: 22 November

Subject 2: inductive types in Coq

Thierry Coquand & Christine Paulin, Inductively defined types, COLOG 1988.
1. Section 1
  Ivo Melse + Mieke van der Meiden: 28 November
2. Sections 2–3
  Jasper Laumen + Tanja Muller: 28 November

Coq Reference Manual: Theory of inductive definitions, 2024.
1. Section "Theory of inductive definitions"
  Sebastian Pack + Max de Boer-Blazdell: 29 November

Subject 3: inductive-recursive types

Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, JSL 65(2), 2000.
1. Sections 1–4
  Dick Arends + Stephan Stanišić: 5 December

Peter Dybjer & Anton Setzer, A Finite Axiomatization of Inductive-Recursive Definitions, TLCA 1999.
1. Sections 3–5
  Bas van der Linden + Remco van Os: 5 December

Subject 4: inductive-inductive types

Fredrik Nordvall Forsberg & Anton Setzer, Inductive-Inductive Definitions, CSL 2010.
1. Sections 3–4
  Thomas Posthuma + Pieter-Jan Lavaerts: 12 December

Ana Bove, Peter Dybjer & Ulf Norell, A Brief Overview of Agda – A Functional Language with Dependent Types, TPHOLs 2009.
1. A demo in Agda of induction-recursion and induction-induction
  (see also Agda User Manual: Mutual Recursion)
  Sophia Lin + Madelief Slaats: 6 December

Subject 5: higher inductive types

Egbert Rijke, Introduction to Homotopy Type Theory, 2020.
1. Chapter 5: "Identity types"
  Joris van der Sluis: 12 December

Peter Dybjer & Hugo Moeneclaey, Finitary Higher Inductive Types in the Groupoid Model, MFPS 2017.
1. Sections 1–3
  Pim Leerkes + Mark Lapidus: 13 December
2. Sections 4–5
  Lyra van Bokhoven + Jasmijn van Tillo: 13 December

Subject 6: quotient inductive-inductive types

Thorsten Altenkirch & Ambrus Kaposi, Type theory in type theory using quotient inductive types, POPL 2016.
1. Sections 1–2
  Tomasz Miśkowicz + Jakub Dreżewski: 19 December
2. Sections 3–4
  Lukas Nieuweboer + Simon Ruiz: 19 December

So the schedule for the presentations is:

21 November	presentation 1	Rutger Broekhoff + Mikhail Ushakov slides tgz
	presentation 2	Niels
22 November	presentation 3	Niels van Duijl + Erik Oosting slides
	explanations	Niels slides slides html coq
25 November	demonstration in Den Haag
28 November	presentation 4	Ivo Melse + Mieke van der Meiden slides
	presentation 5	Jasper Laumen + Tanja Muller slides
29 November	presentation 6	Sebastian Pack + Max de Boer-Blazdell slides
	explanations	Niels slides
5 December	presentation 7	Dick Arends + Stephan Stanišić slides
	presentation 8	Bas van der Linden + Remco van Os slides
6 December	presentation 10	Sophia Lin + Madelief Slaats slides agda agda agda agda
12 December	presentation 9	Thomas Posthuma + Pieter-Jan Lavaerts slides, with pauses
	presentation 11	Joris van der Sluis
13 December	presentation 12	Pim Leerkes + Mark Lapidus slides
	presentation 13	Lyra van Bokhoven + Jasmijn van Tillo slides
19 December	presentation 14	Tomasz Miśkowicz + Jakub Dreżewski slides
	presentation 15	Lukas Nieuweboer + Simon Ruiz slides
20 December	bonus test

5. Coq project

Each student has to do a small Coq 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 Coq project is 24 January 2025.

Grading

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.