- Friday:
**10.45-12.30, HG01.057**

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:

9 september | propositional logic & simple type theory | chapters 1 & 2 |

16 september | predicate logic & dependent types | chapters 4 & 6 |

23 september | inductive types & recursion | chapter 3 |

30 september | inductive predicates & inversion | chapter 3 (continued) |

7 october | program extraction | chapter 5 |

14 october | second-order logic & polymorphism | chapters 7 & 8 |

21 october | inhabitation & summary of the course | chapter 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 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.

- Some slides from 2004:

- Introduction to Type Theory by Herman for additional material

The second half of the course will be taught by Herman Geuvers and Robbert Krebbers. 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:

- Hugo Herbelin, An intuitionistic logic that proves Markov's principle, Proceedings of LICS'10, Edinburgh, p. 50-56, 2010.

The presentations will be held during the first hour, 10.45-11.30. The sections of the paper needs to be presented, and a relevant example worked out (a proof term for a proof, a reduction of a term, etc.) During the second hour, 11.45-12.30, the teachers will go deeper into the material presented.

The current schedule for the presentations is:

11 november | section 11.15 of the Scheme report | Boy Boshoven |

(see also Sussman & Steele and Reynolds) | ||

18 november | section 2 of Sabry & Felleisen | Wouter Smeenk |

25 november | section 3 of Sabry & Felleisen | Fabio Zanasi |

(see also types in the CPS transform) | ||

2 december | sections 2, 3 & 6 of Griffin | Tessa Matser |

9 december | sections 1, 2 & 3 of Krebbers (see also Parigot) | Abel Planting |

13 december | section 2 of Ariola & Herbelin | Matus Tejiscak |

16 december | sections 3 & 4 of Ariola & Herbelin | (Robbert) |

20 december | intro & section 1 of Herbelin | Bas Westerbaan |

(see also a older version of the same paper) | ||

23 december | section 2 of Herbelin | Bram Westerbaan |

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 Herman and Robbert. The test will be

**Tuesday, 17 january 2012, 10.30-12.30, HG00.308**

Some tests:

- test from 2011
- answers to the test from 2011
- test from 2010
- answers to the test from 2010
- test from 2009
- answers to the test from 2009
- test from 2008
- answers to the test from 2008

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.