IMC010: Type Theory and Coq

Teachers

Freek Wiedijk, freek@cs.ru.nl
Herman Geuvers, herman@cs.ru.nl
Niels van der Weide, nweide@cs.ru.nl
Lasse Blaauwbroek, l.blaauwbroek@cs.ru.nl
Robbert Krebbers, robbert@cs.ru.nl
Jules Jacobs, jules.jacobs@ru.nl

Schedule

The course will be taught using Zoom.

The Zoom address will be disseminated through Brightspace. Therefore, if you want to participate in the course, make sure that you are registered there.

Brightspace also will contain videos for the course, and it will be used to send email and keep track of results.

Structure of the course

The course consists of six elements:

1. Lectures about using type theory

Freek will use the first five weeks to teach:

Femke van Raamsdonk, Logical Verification Course Notes

using the schedule:

31 August	introduction & propositional logic	chapter 1
7 September	simple type theory & inductive types	chapters 2 & 3
14 September	predicate logic & dependent types	chapters 4 & 6
21 September	second-order logic & polymorphic types	chapters 7 & 8
28 September	program extraction & inhabitation	chapters 5 & 9

2. Coq practicum

There will be a

Coq practicum corresponding to Femke's course notes

which you can do either in the ProofWeb server (using an ancient version of Coq), as well as in Coq installed on your own machine. For this here is a

zip file with the practicum files

Finishing this practicum is obligatory to be able to pass the course, but there will not be a grade for it. The first person to get all-green traffic lights on the Coq practicum in the ProofWeb server will win a small price.

3. Lectures on some metatheory

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

Herman Geuvers, Introduction to Type Theory

using the schedule:

5 October	principal types and type checking	sections 4.1-4.3, 6.4 slides, exercises, answers
12 October	Church-Rosser property	section 3.1 slides, exercises, answers
19 October	normalization of λ→ and λ2	sections 4.4, 5.6 slides, exercises, answers

This concludes the first half of the course.

4. Exam

As an experiment we will have the exam not 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:

2 November	two hour exam on the theory
3-4 November	individual ten minute oral exam as a follow-up

The exam will be at home without supervision and will be open book/open Coq session. Each student will get a different selection from a larger set of exercises. The answers will have to be submitted through Brightspace as a scan or digital photos.

The exam will be followed by a ten minute oral the days after.

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 a recent research paper, together with a reading list that leads up to this paper.

The topic of the paper this year will be a formal semantics for the Rust programming language, and its formalization in Coq. One of the authors of the paper is Robbert, one of the teachers of the course. The paper is too advanced to fully understand at the level of the course, but we will work on the most important elements.

The presentations are by the students in pairs (and one paper by three students). 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 7 papers that will be presented in 12 presentations are:

The Rust Programming Language
Steve Klabnik and Carol Nichols
- 1. Section 4.1 and 4.2, Section 10.3 (borrows + lifetimes)
- 2. Section 16 (concurrency)
Substructural Type Systems
David Walker
Chapter 1 of "Advanced Topics in Types and Programming Languages" 2005
- 3. Section 1.0-1.2
Separation Logic: A Logic for Shared Mutable Data Structures
John C. Reynolds
LICS 2002
- 4. Section 1-3 (language + assertions)
- 5. Section 4-6 (specifications)
Resources, Concurrency and Local Reasoning
Peter O'Hearn
Theoretical Computer Science 2007
- 6. Section 1-3 (disjoint concurrency)
- 7. Section 4-6 (racy concurrency)
The Type Soundness Theorem That You Really Want to Prove (and now you can)
Derek Dreyer
Video
- 8. All of it
An Introduction to Logical Relations
Lau Skorstengaard
Summer school
- 9. Section 3 (type safety)
- 10. Section 6 (recursive types + step-indexing)
RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers and Derek Dreyer
POPL 2018
Video
Video
- 11. Section 1-3 (type system)
- 12. Section 4-6 (semantic typing)

For help with the first six papers it is best to go to Jules, and about the last paper it is best to ask Robbert.

The presentations will be through the standard Zoom channel on Monday at 08:30 (one presentation per meeting) and on Thursday, also at 08:30 (two presentations per meeting). The schedule for the presentations is:

Mon 23 November	1: Rust	Niek Janssen + Sander Karsten slides
Thu 26 November	2: Rust	Rowan Goemans + Stefan Schrijvers slides, files
	3: Substructural Type Systems	Els Hoekstra + Mirja van de Pol slides
Mon 30 November	4: Separation Logic	Toine Hulshof + Rick van der Wal slides
Thu 3 December	5: Separation Logic	Rob van der Drift + Pieter Cas Kolijn slides
	6: Concurrency	Loes Kruger + Michiel Verloop slides
Mon 7 December	7: Concurrency	Justin Reniers + Johan Sijtsma slides
Thu 10 December	8: Blog post Derek Dreyer	Ruben Holubek + Gunnar Noordbruis slides
	9: Logical Relations	Eline Bovy + Alex van de Griendt + Tosca Klijnsma slides
Mon 14 December	10: Logical Relations	Jeroen Kool + Cárolos Laméris slides
Thu 17 December	11: RustBelt	Luko van der Maas + Ceel Pierik slides
	12: RustBelt	Rick Koenders + Mees Meuwissen slides

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 will be exactly two weeks after the last presentation in the reading group ends.

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.

Experiment

As part of the research in our group, we are developing new, experimental proof automation using Machine Learning for Coq, and we would like you to help us test it. Participation is completely voluntary. Installation and usage instructions can be found here. If you have any questions, you can send an email to l.blaauwbroek@cs.ru.nl, or ask a question on Discord.

What do you get? You get to use our newest automation, which should help you prove the theorems you need for your project more quickly. In particular, there are two new commands. Suggest will recommend some tactics that might be appropriate to use in the current proof state. search will automatically try to finish the current proof for you.

What do we get? The version of Coq you can install from the page above will collect and upload anonymous usage statistics regarding the new automation (such as how often you use it, and under which circumstances). The data we collect will not be traceable to you, and your participation in this experiment will have no bearing on your final grade of Type Theory & Coq. We will also ask you to fill in a short survey at the end of the course.