- Freek Wiedijk, freek@cs.ru.nl
- Herman Geuvers, herman@cs.ru.nl
- Robbert Krebbers, robbert@cs.ru.nl
- Marc Hermes, marc.hermes@ru.nl

Freek will use the first five weeks to teach part of:

- Femke van Raamsdonk, Logical Verification Course Notes

using the schedule:

8 September | introduction & lambda calculus | slides, with pauses |

15 September | propositional logic & simple types | chapters 1 & 2 slides, with pauses coq file |

22 September | predicate logic & dependent types | chapters 4 & 6 slides, with pauses coq file |

29 September | inductive types | chapter 3 slides, with pauses coq file |

6 October | second-order logic & polymorphic types | chapters 7 & 8 slides, with pauses coq file |

There will be a Coq practicum corresponding to Femke's course notes. For this you need to install Coq and download a

- zip file with the practicum files

The completed files need to be handed in in Brightspace. Finishing this practicum is obligatory to be able to pass the course, but there will not be a grade for it.

Then Herman will use the next three weeks to teach part of:

- Herman Geuvers, Introduction to Type Theory

using the schedule:

13 October | principal types & type checking | sections 4.1-4.3, 6.4 slides, exercises, answers |

20 October | Church-Rosser property | section 3.1 slides, exercises, answers |

10 November | normalization of λ→ and λ2 | sections 4.4, 5.6 slides, exercises, answers |

This concludes the first half of the course.

The exam will not be at the end of the course but halfway through. Therefore the subject of the exam will be just the lectures by Freek and Herman, and not the topic of the reading group.

The dates of the exam will be:

17 November 16 January | three hour exam on the theory |

See at the end of this web page for some material to practise for the exam, like old exams from last years.

In the second half of the course we read papers about a specific topic related to a recent research publication (a different topic every year). The topic of this year will be be logical relations.

The presentations are by the students in pairs. These presentations are 45 minutes, and should contain both examples, as well as the gist of the proofs in the paper. It is more important to explain the important points of the paper well, then to cover everything in full detail.

The reading material for this year, together with the students that will present them, are:

- Amal Ahmed, OPLSS 2023: Logical Relations Lecture notes, 2023.
- Section 2 (Termination of STLC, different version than Herman's)
*Joos Munneke + Robert Kunst: 24 November* - Section 3 (Safety of STLC)
*Maud van de Lockant + Susan Withaar: 24 November* - Section 4.0–4.3 (Safety of STLC + μ)
*Lucas van Kasteren + Rico te Wechel: 27 November*

- Section 2 (Termination of STLC, different version than Herman's)

- Andrew W. Appel and David McAllester, An Indexed Model of Recursive Types for Foundational Proof-Carrying Code, TOPLAS, 2001.
- Sections 1–3 (Safety of STLC + μ, "semantic approach")
*Cleo Gerards + Dick Blankvoort: 27 November*

- Sections 1–3 (Safety of STLC + μ, "semantic approach")

- Benjamin Pierce, Types and Programming Languages, MIT Press, 2002.
- Chapter 13 (Semantics/typing of references)
*Jorrit de Boer + Sipho Kemkes: 1 December* - Chapter 24 (Semantics/typing of existential types)
*Quinten Kock + Sijmen van Bommel: 1 December*

- Chapter 13 (Semantics/typing of references)

- Amal Ahmed. Semantics of Types for Mutable State, PhD thesis, Princeton University, 2004.
- Section 2.2 (Safety of STLC + immutable references)
*Patrick van Beurden + Razvan Potcoveanu: 4 December* - Sections 3.1–3.2 (Safety of mutref + ∀/∃, problem + intuitive solution)
*Dmitrii Mikhailovskii + Marijn van Wezel: 4 December* - Section 3.3 (Safety of mutref + ∀/∃, definitions)
*Sergio Domínguez: 8 December*

- Section 2.2 (Safety of STLC + immutable references)

- Philip Wadler, Theorems for free!, FPCA, 1989.
- Sections 1–3 (Parametricity λ2)
*David Logtenberg + Thomas van Bavel: 8 December* - Sections 4–7 (Parametricity λ2)
*Alex van Tilburg + Billy Price: 11 December*

- Sections 1–3 (Parametricity λ2)

- Derek Dreyer, Amal Ahmed and Lars Birkedal, Logical Step-Indexed Logical Relations, LMCS, 2011.
- Sections 1–3 (Binary logrel for mutref + ∀/∃ + μ, Factor step-indexing with ▹ modality)
*Cas Haaijman + Ioannis Koutsidis: 15 December*

- Sections 1–3 (Binary logrel for mutref + ∀/∃ + μ, Factor step-indexing with ▹ modality)

- Amin Timany, Robbert Krebbers, Derek Dreyer and Lars Birkedal,
A Logical Approach to Type Soundness, Under revision for Journal of the ACM.
- Sections 3 and 5 (Data abstraction + logical relations in Iris)
*Lean Ermantraut + Menzo van Kessel: 15 December*

- Sections 3 and 5 (Data abstraction + logical relations in Iris)

So the schedule for the presentations is:

24 November | Termination of STLC | Joos Munneke + Robert Kunst slides |

Safety of STLC | Maud van de Lockant + Susan Withaar slides pptx | |

27 November | Safety of STLC + μ | Lucas van Kasteren + Rico te Wechel slides |

Safety of STLC + μ, "semantic approach" | Cleo Gerards + Dick Blankvoort slides | |

1 December | Semantics/typing of references | Jorrit de Boer + Sipho Kemkes slides |

Semantics/typing of existential types | Quinten Kock + Sijmen van Bommel slides pptx | |

4 December | Safety of STLC + immutable references | Patrick van Beurden + Razvan Potcoveanu slides |

Safety of mutref + ∀/∃ problem + intuitive solution | Dmitrii Mikhailovskii + Marijn van Wezel slides | |

8 December | Safety of mutref + ∀/∃, definitions | Sergio Domínguez slides |

Parametricity λ2 | David Logtenberg + Thomas van Bavel | |

11 December | Parametricity λ2 | Alex van Tilburg + Billy Price notes |

15 December | Binary logrel for mutref + ∀/∃ + μ, Factor step-indexing with ▹ modality | Cas Haaijman + Ioannis Koutsidis |

Data abstraction + logical relations in Iris | Lean Ermantraut + Menzo van Kessel |

Each student has to do a small Coq project. This project can be chosen from

but if students have a suggestion for an interesting project that they want to do, that is also allowed.

The deadline for the Coq project is 20 January 2024.

- exam from 2023
- answers to the exam from 2023
- a second exam from 2023
- answers to the second exam from 2023
- exam from 2022
- answers to the exam from 2022
- exam from 2021
- answers to the exam from 2021
- exam from 2020
- answers to the exam from 2020
- exam from 2019
- answers to the exam from 2019
- exam from 2018
- answers to the exam from 2018
- resit from 2018
- answers to the resit from 2018
- exam from 2017
- answers to the exam from 2017
- exam from 2016
- answers to the exam from 2016
- exam from 2015
- answers to the exam from 2015
- Coq file corresponding to the exam from 2015
- exam from 2014
- answers to the exam from 2014
- exam from 2013
- answers to the exam from 2013
- a second exam from 2013
- answers to the second exam from 2013
- exam from 2012
- answers to the exam from 2012
- exam from 2011
- answers to the exam from 2011
- exam from 2010
- answers to the exam from 2010
- exam from 2009
- answers to the exam from 2009
- exam from 2008
- answers to the exam from 2008