IMC010: Type Theory and Coq



Please make sure that you are registered for this course in Blackboard, as it will be used to send email and administrate results.

Structure of the course

The course consists of five parts:

The basis

We use a course by Femke van Raamsdonk of the Free University Amsterdam. This will be taught by Freek using the following schedule:

3 septemberpropositional logic & simple type theorychapters 1 & 2
13 septemberpredicate logic & dependent typeschapters 4 & 6
20 septembersecond-order logic & polymorphismchapters 7 & 8
27 septemberinductive types & recursionchapter 3
4 octoberwrapping up Femke's coursechapters 5 & 9

The students will be expected to have studied the chapters listed, and the material will be discussed then. You are welcome to ask for help at any time if you have any questions, either by email or by walking into our offices.

The practical work in Coq corresponding to Femke's course will be done using the ProofWeb system on the machine Each participant will get a login to the course page on this machine, and will get his/her password by email.

The relevant links are:

Some metatheory

Next we will go through another (slightly more advanced) introduction to Type Theory. This will be taught by Robbert, using the following schedule:

11 octoberprincipal types and type checkingsections 4.1-4.3, 6.4
18 octoberChurch-Rosser propertysection 3.1
25 octobernormalization of λ→ and λ2sections 4.4, 5.6

This overlaps with Femke's course, and therefore not all sections of the course notes will be discussed in the lectures in detail. (But you do have to know them for the test!)

The relevant links are:

Research topic

After the fall break the course will be taught by Robbert, Herman and Freek together. A research paper or chapter of a book will be studied, together with extra material needed to understand this. Each student will present part of this to the group.

This year the research paper will be on Homotopy Type Theory:

Before we get to this paper, we will study parts of:

The student presentations will be held during the first hour. The assigned part of the paper needs to be presented, and we recommend to explain everything as much as possible through examples. During the second hour, the teachers will go deeper into the material presented.

The current schedule for the presentations is:

12 Nov May 1.1-1.5 mathematical background Jasper
15 Nov Dijkstra 2.1-2.3 identity types, interpretation Wouter
19 Nov HoTT book 1.12 identity types Robbert
22 Nov HoTT book 2.1 types as groupoids Bastiaan
26 Nov HoTT book 2.2-2.3 interpretation →, Π Robbert
29 Nov
Dijkstra 2.4,
HoTT book 3.1
3 Dec no lecture
6 Dec Dijkstra 2.5 higher inductive types Judith
10 Dec HoTT book 3.3, 3.6-3.7 sets, propositions, logic Tim
13 Dec
Dijkstra 2.6,
HoTT book 2.4, 2.10
equivalences, univalence
17 Dec no lecture
20 Dec HoTT book 2.14 equality of structures Jan
7 Jan Dijkstra 3.1 quotients Ennier
10 Jan HoTT book 7.2 UIP, Hedberg Robbert
14 Jan Circle paper II-IV basics Robbert
17 Jan Circle paper V proof Niels

Some other (maybe relevant) links about Homotopy Type Theory:

Individual Coq exercise

Each student will be doing a small Coq formalization assignment. This assignment will be chosen by the student from the following list of suggestions.

Final test

The test covers both the contents of the courses by Femke and Robbert, as well as the contents of the research paper. The first test opportunities will be:

Some older tests:

See the "exercises on paper" above too, which are also exercises from old tests.


Each participant will get three grades: one for the presentation in the second half of the course, one for the individual Coq exercise, and one for the test. The final grade will be the average of these three grades.

There will be no grade for the practical work for Femke's course in ProofWeb, but this work will need to be finished to be allowed to pass the course.

Some supporting material