Freek will use the first five weeks to teach part of:
using the schedule:
6 September | introduction & lambda calculus | |
13 September | propositional logic & simple types | chapters 1 & 2 |
20 September | predicate logic & dependent types | chapters 4 & 6 |
27 September | inductive types & inductive predicates | chapter 3 |
4 October | second-order logic & polymorphic types | chapters 7 & 8 |
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:
11 October | principal types & type checking | sections 4.1-4.3, 6.4 slides, exercises, answers |
18 October | Church-Rosser property | section 3.1 slides, exercises, answers |
8 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:
16 November | two hour exam on the theory in E 2.50 |
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 papers about a specific topic related to a recent research publication (a different topic every year). The topic of this year will be cubical type theory.
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 book and papers for this year, together with the students that will present them, are:
So the schedule for the presentations is:
30 November | path induction | Aron Schöffer & Tjitske Koster slides |
equivalence, higher groupoids | Gé Waayers & Nick Hendriks slides | |
6 December | universes, univalence | Niels van der Weide slides |
application of univalence | Daniël van Leijenhorst & Finn van der Velde slides | |
7 December | h-levels, truncation | Niek Terol & Thomas Somers slides |
examples of HITs | David Läwen & Jakob Wuhrer slides | |
13 December | path types | Bryan van de Ven & Cas Visser slides |
operations on paths | Daan Spijkers & Samuel Klumpers slides | |
14 December | glue types | Mika van Emmerloot & Marten Straatsma slides |
Agda | Alwyn Stiles & Eef Uijen slides sources | |
20 December | Cubical Agda | Dante van Gemert & Paul Tiemeijer slides |
the paper | Aron van Hof & Bram Pellen slides | |
21 December | structure identity principle | Gerbrich Kroon & Rutger Dinnissen slides |
using the principle | Alex van der Hulst & Simcha van Collem slides |
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 20 January 2023.