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
19 OctoberChurch-Rosser propertysection 3.1
slides, exercises, answers
9 Novembernormalization of λ→ and λ2sections 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 date of the exam will be:

19 Novembertwo hour exam on the theory in HG00.307 

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 about recent research. The topic of the papers this year is the Lean system.

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 papers for this year, together with the students that will present them, are:

  1. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura, A metaprogramming framework for formal verification. PACMPL, 2017.
    Markel Zubia: 10 December
  2. Alex Reinking, Ningning Xie, Leonardo de Moura, Daan Leijen, Perceus: Garbage Free Reference Counting with Reuse, PLDI 2021: Programming Language Design and Implementation.
    Kirsten Hagenaars & Astrid van der Jagt: 14 December
  3. Daniel Selsam, Simon Hudon, Leonardo de Moura, Sealing Pointer-Based Optimizations behind Pure Functions. Proc. ACM Program. Lang., 2020.
    Buster Bosma & Michiel Philipse: 14 December
  4. Daniel Selsam, Sebastian Ullrich, Leonardo de Moura, Tabled Typeclass Resolution. 2020.
    Dor Alter & Orpheas van Rooij: 17 December
  5. Sebastian Ullrich, Leonardo de Moura, Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, 2020.
    (not assigned)
  6. The mathlib community, The Lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20–21, 2020, 2020.
    Stijn van den Beemt & Willem Lambooij: 17 December
  7. Eric Wieser, Scalar actions in Lean's mathlib. 2021.
    Steven Bronsveld & Jelmer Firet: 21 December
  8. Mario Carneiro, Porting Mathlib (talk), Formal Mathematics for Mathematicians (FMM) 2021.
    (not assigned)
  9. Mario Carneiro, Formalizing Computability Theory via Partial Recursive Functions. 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9–12, 2019, Portland, OR, USA, 2019.
    Robin Holen & Mirja van de Pol: 21 December

So the schedule for the presentations is:

30 NovemberLean demoSuzan Erven &
Amber Pater
slides
3 Decemberclassical axiomsMenno Bartels &
Roy Willems
slides
typing rulesJeroen van Wees
slides slides
7 DecemberundecidabilityWietze Koops &
Niels Vooijs
slides
W typesBálint Kocsis &
Márk Széles
slides lean
10 DecemberZFC modelThijs van Loenhout &
Sander Suverkropp
slides
metaprogrammingMarkel Zubia
slides
14 Decemberreference countingKirsten Hagenaars &
Astrid van der Jagt
pointersBuster Bosma &
Michiel Philipse
slides
17 Decembertypeclass resolutionDor Alter &
Orpheas van Rooij
slides
MathlibStijn van den Beemt &
Willem Lambooij
slides
21 Decemberscalar actionsSteven Bronsveld &
Jelmer Firet
computability theoryRobin Holen &
Mirja van de Pol

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 is 19 January 2022.

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

Coq support from Jules

Paper exercises

Old exams

Some slides