Freek will use the first five weeks to teach:
using the schedule:
7 September | introduction & propositional logic | chapter 1 |
17 September | simple type theory & inductive types | chapters 2 & 3 |
24 September | predicate logic & dependent types | chapters 4 & 6 |
1 October | second-order logic & polymorphic types | chapters 7 & 8 |
8 October | program extraction & inhabitation | chapters 5 & 9 |
There will be a Coq practicum corresponding to Femke's course notes. For this you need to install Coq and download a
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.
Then Herman will use the next three weeks to teach part of:
using the schedule:
15 October | principal types and type checking | sections 4.1-4.3, 6.4 slides, exercises, answers |
19 October | Church-Rosser property | section 3.1 slides, exercises, answers |
9 November | normalization of λ→ and λ2 | sections 4.4, 5.6 slides, exercises, answers |
This concludes the first half of the course.
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 and Herman, and not the topic of the reading group.
The date of the exam will be:
19 November | two hour exam on the theory in HG00.307 |
See at the end of this web page for some material to practise for the exam, like old exams from last years.
In the second half of the course we read about recent research. The topic of the papers this year is the Lean system.
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 papers for this year, together with the students that will present them, are:
So the schedule for the presentations is:
30 November | Lean demo | Suzan Erven & Amber Pater slides |
3 December | classical axioms | Menno Bartels & Roy Willems slides |
typing rules | Jeroen van Wees slides slides | |
7 December | undecidability | Wietze Koops & Niels Vooijs slides |
W types | Bálint Kocsis & Márk Széles slides lean | |
10 December | ZFC model | Thijs van Loenhout & Sander Suverkropp slides |
metaprogramming | Markel Zubia slides | |
14 December | reference counting | Kirsten Hagenaars & Astrid van der Jagt |
pointers | Buster Bosma & Michiel Philipse slides | |
17 December | typeclass resolution | Dor Alter & Orpheas van Rooij slides |
Mathlib | Stijn van den Beemt & Willem Lambooij slides | |
21 December | scalar actions | Steven Bronsveld & Jelmer Firet |
computability theory | Robin Holen & Mirja van de Pol |
Each student has to do a small Coq project. This project can be chosen from
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 19 January 2022.