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.
The course has five parts:
We use a course by Femke van Raamsdonk of the Free University Amsterdam. This will be taught by Freek using the following schedule:
| 4 February | introduction & propositional logic | chapter 1 |
| 14 February | simple type theory & inductive types | chapters 2 & 3 |
| 21 February | predicate logic & dependent types | chapters 4 & 6 |
| 28 February | second-order logic & polymorphic types | chapters 7 & 8 |
| 6 March | program extraction & inhabitation | chapters 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 prover.cs.ru.nl. 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:
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 March | principal types and type checking | sections 4.1–4.3, 6.4 slides, exercises, answers |
| 20 March | Church-Rosser property | section 3.1 exercises, answers |
| 17 April | normalization of λ→ and λ2 | sections 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:
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:
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) slides |
| Tuesday 26 May, 10:30 | Lea Nugteren + Maaike Heijdenrijk | 2: Coq Manual (Sections 4.4.1-4.4.4) slides |
| Gregor Alexandru + Jochem Raat | 2: Coq Manual (Section 4.4.5) slides |
|
| 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!
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.
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.