Please make sure that you are registered for this course in Blackboard, as it will be used to send email and administrate results.
The course consists of 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:
| 6 february | propositional logic & simple type theory | chapters 1 & 2 |
| 20 february | predicate logic & dependent types | chapters 4 & 6 |
| 27 february | second-order logic & polymorphism | chapters 7 & 8 |
| 6 march | inductive types & recursion | chapter 3 |
| 13 march | inductive predicates & inversion | 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. This will be taught by Herman, using the following schedule:
| 20 march | principal types and type checking | sections 4.1-4.3, 6.4 slides, exercises |
| 27 march | Church-Rosser property | section 3.1 exercises |
| 17 april | normalization of λ→ and λ2 | sections 4.4, 5.6 slides, exercises |
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 Dan, Herman and Freek together. A research paper will be read, together with extra material needed to understand it. The research paper for this year will be on the CPS translation:
More specifically, we will look at the following subjects:
As preparation for the research paper, we will study parts of a course about compilation of functional programming languages, and then read two other papers first:
Each student will present his or her part of the material to the group for 45 minutes. Slides are not required, but are allowed. If possible you should explain everything through examples, and you should be understand the proofs and for example if a proof is by induction present one of the interesting cases. If time permits, after the presentations the teachers will expand on what has been presented.
The current schedule for the presentations is:
| 24 april | Leroy I: 1–19 | Bas Broere | slides |
| 8 may | Leroy III: 50–57, 62–63 | Jan Martens | slides |
| Leroy III: 64–70, 74–75 | Tom Nikken | slides | |
| 15 may | H-L (A): 1–3 | Vincent Koppen | slides |
| H-L (A): 4 intro, 4.2 | Jelte Zwetsloot | slides | |
| 22 may | no presentations | ||
| 29 may | H-L (A): 4.1, 4.3–4.4 | Bas Swinkels | slides |
| 5 june | H-L (B): 1–3 | Daniil | |
| H-L (B): 4 excluding 4.4 | Marnix Suilen | slides | |
| 12 june | H-L (B): 5 | Aldo Gunsing | slides |
| B-H-S: 2 | Haye Böhm | slides | |
| B-H-S: 3 | Flip van Spaendonck | slides | |
| 19 june | B-H-S: 4 intro, 4.1 | Camil Staps | slides |
| B-H-S: 4.2 | René den Hertog |
Feel free to exchange presentation slots if you like, but if you do this then please tell Freek, so the schedule will stay up to date. Also, if you need help with preparing your presentation, contact one of the teachers in time.
For additional reading, you also might look at:
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 test covers both the contents of the courses by Femke and Herman, as well as the contents of the presentations. The final test 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 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.