IMC010: Type Theory and Coq

Teachers

Location

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.

Structure of the course

The course consists of five parts:

The basis

We use a course by Femke van Raamsdonk of the Free University Amsterdam. This will be taught by Freek using the following schedule:

29 Januarypropositional logic & simple type theorychapters 1 & 2
4 Februarypredicate logic & dependent typeschapters 4 & 6
11 Februarysecond-order logic & polymorphismchapters 7 & 8
18 Februaryinductive types & recursionchapter 3
25 Februaryinductive predicates & inversionchapters 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:

Some metatheory

Next we will go through another (slightly more advanced) introduction to Type Theory. This will be taught by Herman, using the following schedule:

11 Marchprincipal types and type checkingsections 4.1–4.3, 6.4
slides, exercises
8 AprilChurch-Rosser propertysection 3.1
exercises
15 Aprilnormalization of λ→ and λ2sections 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:

Research topic

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:

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

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
7 May 13.30 Atkey-McBride, sec 1 Ilse Pool +
Jeroen Slot
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 June 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 +
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.

Individual Coq exercise

Each student will be doing a small Coq formalization assignment. This assignment will be chosen by the student from the following list of suggestions.

Final test

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:

Some old tests:

See the "paper exercises" above too, which are also exercises from old tests.

Grading

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.

Some supporting material