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 four parts:
We use the course by Femke van Raamsdonk of the Free University Amsterdam: This will be taught by Freek using the following schedule:
| 3 september | propositional logic & simple type theory | chapters 1 & 2 |
| 10 september | predicate logic & dependent types | chapters 4 & 6 |
| 17 september | inductive types & recursion | chapter 3 |
| 24 september | inductive predicates & inversion | chapter 3 (continued) |
| 1 october | program extraction | chapter 5 |
| 8 october | second-order propositional logic | chapter 7 |
| 15 october | polymorphism | chapter 8 |
| 22 october | inhabitation & summary of the course | chapter 9 |
During this period there only will be contact hours on the Fridays. 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 second half of the course will be taught by James McKinna and Herman Geuvers. 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:
Actually, The view from the left has two versions, and we will in the course focus on the "draft" version that was not published. This means that the papers that we will read are:
A VDI by Carst Tankink for running Epigram in Virtual Box:
Installation via Virtual Box. Use in the wizard an existing disk. Username and password are both "default", and Epigram can be started from the folder on the desktop.
Two example files by James showing how to do Wadler's views in Epigram and in Coq:
For this part of the course we will use the following schedule:
| 9 november | introduction to The view from the left | Herman |
| 16 november | Wadler's paper = paper 1 | Carsten Rütz |
| 23 november | Epigram: demo & papers 2 and 3 | Bob van der Linden |
| 30 november | chapter 3 from paper 4 | Frank Roumen |
| 7 december | chapter 4 from paper 4 | Remy Viehoff |
| 14 december | chapter 5 from paper 4 | Boy Boshoven |
| 21 december | chapter 7 from paper 4 | Brinio Hond |
| 11 january | recapitulation of The view from the left | Herman & James |
Each time apart from 9 november and 11 january a student will present material during the first hour, and then Herman and James will continue on that in the second hour.
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 course by Femke as well as the contents of the research paper taught by James and Herman. 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 part of the course, one for the Coq work, 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.