IMC010: Type Theory and Coq



Please make sure that you are registered for this course in Brightspace, as it will be used to send email and keep track of results.

Structure of the course

The course has five parts:

  1. The basis of type theory
  2. Some metatheory
  3. Research paper presentations
  4. individual Coq project
  5. Exam

The basis of type theory

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

4 Februaryintroduction & propositional logicchapter 1
14 Februarysimple type theory & inductive typeschapters 2 & 3
21 Februarypredicate logic & dependent typeschapters 4 & 6
28 Februarysecond-order logic & polymorphic typeschapters 7 & 8
6 Marchprogram extraction & inhabitationchapters 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 during the lectures.

The relevant links are:

Some metatheory

Next we will go through another (slightly more advanced) introduction to Type Theory. The plan was that these would be taught by Herman, using the following schedule:

13 Marchprincipal types and type checkingsections 4.1–4.3, 6.4
slides, exercises, answers
20 MarchChurch-Rosser propertysection 3.1
exercises, answers
17 Aprilnormalization of λ→ and λ2sections 4.4, 5.6
slides, exercises, answers

However, because of the corona virus, these lectures will not be taught this year. Instead you should watch the web-lectures from 2018-2019, under "Content" in Brightspace. If you have any questions about these lectures, you can mail Herman or Freek.

This material 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 paper presentations

After the May vacation the course will be taught by Freek, Herman, Dan, Niels and Lasse together. A research paper will be read, together with extra material needed to appreciate it.

The research paper for this year is part of the MetaCoq and CertiCoq projects, and is about formalizing the type theory of Coq in Coq and using that as a basis for implementing Coq (at a later stage) and Coq plug-ins (now already) in the language of Coq instead of in OCaml (which is the current implementation language):

This work opens the road to an implementation of Coq that is proved to be correct using Coq itself.

The papers that we will read (of which the first two are actually book chapters) are:

  1. Yves Bertot, Pierre Castéran, Coq'Art: The Calculus of Inductive Constructions, Chapter 16: Proof by Reflection, EATCS, Springer, 2004.
  2. The Coq Development Team, The Coq Reference Manual, Section 4.4, version 8.11.0, January 2020.
  3. Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau, The next 700 syntactic models of type theory, CPP 2017.
  4. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau, Towards Certified Meta-Programming with Typed Template-Coq, ITP 2018.
  5. Vadim Zaliva, Matthieu Sozeau, Reification of shallow-embedded DSLs in Coq with automated verification, extended abstract, CoqPL 2019. Git repository of the paper, and updated repository that works with the latest Coq and MetaCoq.
  6. Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock, QED at large, Foundations and Trends in Programming Languages, 5(2-3), 2019.
  7. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter, The MetaCoq Project, extended version of paper 4, 2019.
  8. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter, Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq, POPL 2020. POPL talk.

Below we give an overview of why we selected these papers and how they hang together.

The schedule of the presentations of these papers is:

Tuesday 19 May, 10:30 Marene Dimmendaal
+ Pleun Koldewijn
1: Coq'Art
(Chapter 16)
Tuesday 26 May, 10:30 Lea Nugteren
+ Maaike Heijdenrijk
2: Coq Manual
(Sections 4.4.1-4.4.4)
Gregor Alexandru
+ Jochem Raat
2: Coq Manual
(Section 4.4.5)
Friday 29 May, 13:30 Giacomo Bruno
+ Ruben Turkenburg
3: 700 syntactic models
(Sections 1-3, 5.1)
Job Cuppen
+ Steven van der Vorm
4: Template-Coq
(without 5.2)
Tuesday 2 June, 10:30 Gijs van Cuyck
+ Mees van Osch
5: Reification of DSLs
+ demo of Coq code
Danish Alvi
+ Herman Bergwerf
6: QED at large
(Chapters 3-4)
Friday 5 June, 13:30 Bob Ruiken
+ Justin Reniers
6: QED at large
(Chapter 5)
Bart Sol
+ Colin de Roos
7: The MetaCoq Project
(up to Section 2)
Tuesday 9 June, 10:30 Gijs Alberts
+ Jonas Kamminga
7: The MetaCoq Project
(Section 4 and further)
Tom Sweers
+ Wieke Bergers
8: Coq Coq Correct!
(up to Section 2)
Friday 12 June, 13:30 Marck van der Vegt 8: Coq Coq Correct!
(Section 3)
Simone Waning
+ Wessel de Weijer
8: Coq Coq Correct!
(Section 4)

Each paper will presented by two (or in one case: three) students for the other students for 45 minutes, as a Zoom session. The URL for this is:

The password will be disseminated through Brightspace. This year slides are required, as there will not be a blackboard to write on. If time permits, after the presentations the teachers might expand on what has been presented.

We encourage you to contact the teachers when preparing for your presentations!

Overview of the reading list

We now give a very brief overview of the "Coq Coq Correct!" paper (paper 8). It consists of three main parts:

Although it is not actually part of the "Coq Coq Correct!" paper, we also will study another important part of the MetaCoq project:

Finally, as more general background for the "Coq Coq Correct!" paper, we will also read part of the recent "QED at large" paper (paper 6), which presents a bigger picture around the MetaCoq and CertiCoq projects.

Individual Coq project

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


The exam covers both the contents of the courses by Femke and Herman, as well as the contents of the presentations. The exam and resit will be:

Some old tests:

See the "paper exercises" 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 project, 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