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:
| 7 september | propositional logic & simple type theory | chapters 1 & 2 |
| 14 september | predicate logic & dependent types | chapters 4 & 6 |
| 21 september | second-order logic & polymorphism | chapters 7 & 8 |
| 28 september | inductive types & recursion | chapter 3 |
| 12 october | no lecture |
(The last lecture is delayed by one week because Herman is not available on the 12th, so we shifted his first lecture – see below – to the 5th.)
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 proofweb.cs.ru.nl. Each participant will get a login to the course page on this machine, and will get his/her password by email.
The relevant links are:
Next we will go through another introduction to type theory by Herman. This will be taught by Herman, using the following schedule:
| 5 october | principal types and type checking | sections 4.1-4.3, 6.4 | slides |
| 19 october | Church-Rosser property | section 3.1 | exercise |
| 26 october | normalization of λ→ and λ2 | sections 4.4, 5.6 | slides |
The course 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 fall break the course will be taught by Herman and Freek together. A research paper will be studied, together with extra material needed to understand this research paper. Each student will present part of this to the group.
This year the research paper will be:
The presentations will be held during the first hour, 15.45-16.30. The assigned part of the paper needs to be presented, and a relevant example worked out. During the second hour, 16.45-17.30, the teachers will go deeper into the material presented.
The current schedule for the presentations is:
| 16 november | introduction | Freek & Herman |
| 23 november | Coq'Art, 14.1.1-14.1.3 | Wessel van Staal slides |
| 30 november | Coq'Art, 14.1.4-14.1.5 | Rob Tiemens slides |
| 7 december | Inductive Definitions in the System Coq, 1 & 2 | Joshua Moerman |
| 14 december | The Coq Proof Assistant Reference Manual, 4.5 | Robbert |
| 18 december in HG02.702 | On a few open problems of the Calculus of Inductive Constructions (workshop talk) | Freek & Robbert |
| 21 december | The guard condition of Coq (workshop talk) | Kelley van Evert |
| 8 januari in HG02.702 | Matita | Alex Brouwers |
| 11 januari | The Construcive Engine (workshop talk) | Markus Klinik slides |
| 18 januari | A compact kernel for the calculus of inductive constructions & A bi-directional refinement algorithm for the Calculus of (Co)Inductive Constructions | Herman |
Note that there will be one extra meeting on Tuesday 4 december.
Also, the book Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions is copyrighted, and so we cannot put the relevant pages here.
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 research paper. The test will be
Some tests:
See the "exercises on paper" 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.