IMC010: Type Theory and Coq

Teachers

Structure of the course

The course consists of six elements:

1. Lectures on using type theory

Freek will use the first five weeks to teach:

using the schedule:

7 Septemberintroduction & propositional logicchapter 1
17 Septembersimple type theory & inductive typeschapters 2 & 3
24 Septemberpredicate logic & dependent typeschapters 4 & 6
1 Octobersecond-order logic & polymorphic typeschapters 7 & 8
8 Octoberprogram extraction & inhabitationchapters 5 & 9

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

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 some metatheory

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

using the schedule:

15 Octoberprincipal types and type checkingsections 4.1-4.3, 6.4
slides, exercises, answers
22 OctoberChurch-Rosser propertysection 3.1
slides, exercises, answers
12 Novembernormalization of λ→ and λ2sections 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 date of the exam will be:

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

The topic of the paper this year has not been decided yet. We are considering looking at the Lean system.

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.

6. Coq project

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 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.

Some supporting material

Paper exercises

Old exams

Some slides