- Freek Wiedijk, freek@cs.ru.nl, M1.03.04
- Herman Geuvers, herman@cs.ru.nl, M1.00.05
- Daniil Frumin, dfrumin@cs.ru.nl, M1.03.03
- Niels van der Weide, nweide@cs.ru.nl, M1.01.08A

- Monday:
**15.30-17.15, HG00.071 (until 11 March) and HG00.062 (8 and 15 April)**

Please make sure that you are registered for this course in Brightspace, as it will be used to send email and keep track of 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:

29 January | propositional logic & simple type theory | chapters 1 & 2 |

4 February | predicate logic & dependent types | chapters 4 & 6 |

11 February | second-order logic & polymorphism | chapters 7 & 8 |

18 February | inductive types & recursion | chapter 3 |

25 February | 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:

11 March | principal types and type checking | sections 4.1–4.3, 6.4 slides, exercises |

8 April | Church-Rosser property | section 3.1 exercises |

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

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

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 *guarded type theory*:

- Niccolò Veltri and Niels van der Weide, Guarded Recursion in Agda via Sized Types, submitted to FSCD 2019 (see also the git repository)

As preparation for the research paper, we will read a chapter from a book and four other papers first:

- Yves Bertot and Pierre Castéran, Coq'Art: The Calculus of Inductive Constructions, Chapter 13
- Robert Atkey and Conor McBride, Productive Coprogramming with Guarded Recursion, ICFP 2013
- Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl and Lars Birkedal, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, LMCS 2016
- Andreas Abel, MiniAgda: Integrating Sized and Dependent Types, EPTCS 43, 2010 (ITP Workshop)
- Andreas Abel, Brigitte Pientka, David Thibodeau and Anton Setzer, Copatterns: programming infinite structures by observations, POPL 2013

Each paper will presented by two students for the group for 45 minutes. Slides are not required, but are allowed. Everything should be explained through examples (if possible), and you should be understand and explain the proofs (for example in a proof by induction you could present one of the interesting cases in more detail). If time permits, after the presentations the teachers will expand on what has been presented.

The current schedule for the presentations is:

23 April | 13.30 | Coq'Art, Ch 13.1–13.3 | Erik Voogd + Jan Heemstra | |

23 April | 14.30 | Coq'Art, Ch 13.4–13.5 | Cas Spaans + Margot Albers | |

23 April | 15.30 | Coq'Art, Ch 13.6–13.7 | Koen Timmermans + Marnix Suilen + coq | |

7 May | 13.30 | Atkey-McBride, sec 1 | Ilse Pool + Jeroen Slot + text | |

7 May | 14.30 | Atkey-McBride, sec 2 | Frank Gerlings + Serena Rietbergen | |

7 May | 15.30 | Atkey-McBride, sec 3 | Flip van Spaendonck + Joep Veldhoven | |

14 May | 13.30 | Clouston et al., sec 1 | Kasper Hagens + Nikki Jaspers | |

21 May | 13.30 | Abel, sec 1–2 | Loes Habermehl + Luuk Verkleij | |

21 May | 14.30 | Abel, sec 3–4 | Edoardo Putti + Lorena Yunes Arriaga | |

28 May | 13.30 | Abel et al., sec 1–2 | Bas Hofmans + Joris den Elzen | |

28 May | 14.30 | Abel et al., sec 3–4 | Folkert de Vries + Stephen Ellis | |

4 June | 13.30 | Veltri-vdWeide, sec 1+3 | Jonathan Moerman + Jos Craaijo | |

4 June | 14.30 | Veltri-vdWeide, sec 4 (+ intro Kripke semantics) | Dirk van Bree + Marein Könings + Timo Maarse | |

4 June | 15.30 | Veltri-vdWeide, sec 5 | Coen Borghans + Frank van Hoof |

If you want help with preparing your presentation (recommended!), contact one of the teachers in time.

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:

**Tuesday, 11 June 2019, 8.30-11.30, HG00.307**(HG00.310 for extra time)

Some old tests:

- test from 2019
- answers to the test from 2019
- resit from 2019
- answers to the resit from 2019
- test from 2018
- answers to the test from 2018
- test from 2017
- answers to the test from 2017
- test from 2016
- answers to the test from 2016
- Coq file corresponding to the test from 2016
- 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: