IMC010: Type Theory and Coq

Teachers

Structure of the course

The course consists of six parts:

1. Lectures on the type theory of Coq

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

2. Coq practicum

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.

3. Lectures on metatheory

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.

4. Exam

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.

5. Reading group with presentations

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.
1. Section 2 (Termination of STLC, different version than Herman's)
  Joos Munneke + Robert Kunst: 24 November
2. Section 3 (Safety of STLC)
  Maud van de Lockant + Susan Withaar: 24 November
3. Section 4.0–4.3 (Safety of STLC + μ)
  Lucas van Kasteren + Rico te Wechel: 27 November

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

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

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

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

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

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

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

6. Coq project

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

list of possible projects

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.

Grading

You will get three marks: for the exam, the Coq presentations, and the Coq project (items 4, 5 and 6 above). The final mark for the course is the average of those three marks, rounded to a half integral number. A mark of 5.5 will be rounded up to 6, and the mark for the exam has to be at least 5.0.