- Friday:
**13.45-15.30, HG01.029**(first half of the course) - Friday:
**10.45-12.30 & 13.45-15.30, M1.00.02**(second half of the course)

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:

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

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

19 september | second-order logic & polymorphism | chapters 7 & 8 |

26 september | inductive types & recursion | chapter 3 |

3 october | wrapping up Femke's course | 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 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 (slightly more advanced) introduction to Type Theory. This will be taught by Herman, using the following schedule:

10 october | principal types and type checking | sections 4.1-4.3, 6.4 | slides exercises |

17 october | Church-Rosser property | section 3.1 | exercises |

24 october | normalization of λ→ and λ2 | sections 4.4, 5.6 | slides exercises |

This 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:

- The course notes by Herman
- The Church-Rosser proof by Masako Takahashi (only Section 1 is relevant)

After the fall break the course will be taught by Robbert, Herman and Freek together. A research paper or chapter of a book will be studied, together with extra material needed to understand this. Each student will present part of this to the group.

This year the research paper will be on *normalization by evaluation*:

- Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire, Full reduction at full throttle

Before we get to this paper, we will study parts of:

- Martijn Oostdijk, Herman Geuvers, Proof by Computation in the Coq system
- Christine Paulin-Mohring, Introduction to the Coq proof-assistant for practical software verification
- Benjamin Grégoire, Assia Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq
- Benjamin Grégoire, Xavier Leroy, A Compiled Implementation of Strong Reduction
- Georges Gonthier, Formal Proof—The Four-Color Theorem

The student presentations will be held during the first hour. The assigned part of the paper needs to be presented, and we recommend to explain everything as much as possible through examples. During the second hour, the teachers will go deeper into the material presented.

The current schedule for the presentations is:

28 november | Oostdijk/Geuvers section 4 | Rafael Alejandro Imamgiller |

28 november | Paulin-Mohring section 5.3 | Timothy Fraser |

5 december | Grégoire/Mahboubi sections 2-3 | Timmy Weerwag |

5 december | Grégoire/Leroy sections 2.1-2.2 | Suzanne van den Bosch |

12 december | Grégoire/Leroy section 2.3 | Rik de Kort |

12 december | Grégoire/Leroy section 3 | Fenno Vermeij |

19 december | Boespflug/Dénès/Grégoire section 1 | Maxime Klusman |

19 december | Boespflug/Dénès/Grégoire section 2 | Gerco van Heerdt |

9 january | Gonthier before combinatorial hypermaps | Jasper Piers |

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 first test opportunity will be:

**Tuesday, 26 January 2015, 14.00-17.00, HG00.086**

Some tests:

- test from 2014
- answers to the test from 2014
- test from 2013
- answers to the test from 2013
- a second test from 2013
- answers to the second test from 2013
- test from 2012
- answers to the test from 2012
- 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 "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.

- Slides for a course from fall 2004:

- Slides for a course from spring 2012: