IMC010: Type Theory and Coq

Teachers

• Freek Wiedijk
• James McKinna
• Herman Geuvers

Rooms

• Tuesday: 10.45-12.30, HG01.057
• Friday: 15.45-16.30, LIN 7

Please make sure that you are registered for this course in Blackboard, as it will be used to send email and administrate results.

An impression

Structure of the course

The course consists of four parts:

The basis

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

22 september	propositional logic & simple type theory predicate logic & dependent types	chapters 1 & 2 chapters 4 & 6
29 october	inductive types	chapter 3
6 october	no lecture
13 october	second-order propositional logic & polymorphism	chapters 7 & 8
20 october	program extraction & inhabitation	chapters 5 & 9

During this period there only will be contact hours on the Tuesdays. 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 proofweb.cs.ru.nl. Each participant will get a login to the course page on this machine, and will get his/her password by email.

• The course notes
• The exercises on ProofWeb

• Exercises on paper 1
• Exercises on paper 2

• Some slides from 2004:
  1. propositional logic
  2. simply typed λ-calculus
  3. normalization & classical logic
  4. inductive types
  5. inductive predicates
  6. predicate logic
  7. program extraction
  8. dependent types
  9. the pure type system called λP
  10. polymorphism and impredicativity
  11. second order propositional logic
  12. λ2

Advanced topics

In the second half of the course, advanced topics will be taught by James McKinna and Herman Geuvers. The schedule for this part of the course is:

10 november	varieties of type theory	(James)
17 november	strong normalization for STT and lambda 2	(Herman)
24 november	overview of the meta-theory of PTSs, including type checking	(Herman)
1 december	semantics of inductive types	(James)
8 december	type theory for mathematics	(Herman)
15 december	dependently typed functional programming	(James)

• Herman's slides about strong normalization for STT and lambda 2
• Herman's slides about meta-theory of PTSs, including type checking
• Herman's slides about type theory for mathematics
• Herman's lecture notes (the 17 november handout was pages 26-30 and 41-43, and the 24 november handout was pages 50-56)
• Herman's paper "Modular proof of strong normalization for the calculus of constructions"
• Herman's example Coq file
• James' slides about Epigram
• James' example Epigram files: natural numbers and Takahashi's confluence proof for combinatory logic
• some pages from Davey & Priestley's "Introduction to Lattices and Order" with lots of definitions leading up to the Knaster-Tarski fixpoint theorem (the proofs of theorem 4.11 and lemma 4.13)

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.

The final test

The test covers both the contents of the course by Femke as well as the advanced topics taught by James and Herman. The test will be

• Thursday 21 January 2010, 15.30-17.30, HG00.308

Grading

Each participant will get two grades: one for the Coq work, and one for the test. The final grade will be the average of these two grades.