As the name indicates, we will spend the semester reading papers on Curry-Howard correspondence, type systems and type theories. This should be of particular interest to students who completed the SemProg course or are otherwise familiar with proof assistants or dependent types. Students with knowledge of functional programming are also a natural audience. We will learn what makes proof assistants work and what are superficial and deep differences between most famous ones like Coq and Agda. Depending on interests and competences of participants, we can also focus more on issues like metaprogramming, code generation, GADTs, programming semantics and computational effects.

The papers we are going to study will allow students to recognize and explain key features and differences between respective theoretical underpinnings of proof assistants like Coq or Agda. The students will be able to explain why these systems (e.g., calculus of constructions, Martin-Löf type theory) are normalizing/terminating, compare the benefits and disadvantages of adding new constructs and give examples of safe and unsafe extensions of corresponding systems.

We will read

• Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry–Howard isomorphism, Studies in Logic and the Foundations of Mathematics 149, Elsevier Science, ISBN 978-0-444-52077-7.

Please note that we are linking now to the published version (freely accessible if you’re on campus) which is very different to the old draft @ citeseer! It’d be misleading for us and unfair to the authors to use that old draft (which, sadly, wikipedia links to, for example), as clearly many things have been improved and changed for the published version after that early draft appeared. The final product is a really different (and obviously better) book. Thanks to Thorsten for pointing this out.

1. 24 X: Chapter 1. As Daniel is not going to attend, Daniel (G.) was an emergency replacement. Note that in old citeseer draft which we mistakenly began to use, the authors were running into some problems with their structural induction/recursion in presence of binding, renaming and free variables: you can see, for example, how they originally handled the definition of free variable of a term (as opposed to preterm) and compare it with the finally published version. For an extended discussion of such issues one can see, for example, Andrew Pitts tutorial slides of MGS 2011. Another approach can be found in a famous Fiore, Plotkin and Turi paper. What these papers have in common can appreciated by those familiar with the contents of Stefan’s course: it is taking the initial algebra approach one step further, to syntax with binding. However, if the issue is just finding canonical representatives of alpha-equivalence classes, then there is a standard technique applied in CS which does not require using too abstract categorical/algebraic apparatus: via so-called de Bruijn indices. And for an alternative introduction to lambda calculus than this first chapter, see these notes of Barendregt and Barendsen.
2. 31 X: We discussed Chapter 2. I distributed another Chapter 2—of Chagrov & Zakharyaschev book on modal logic—as an additional reference.
3. 7 XI: We will finish discussing Chapters 1 and 2, then hopefully Thorsten will begin with Chapter 3. I’m beginning to suspect that one chapter per seminar is an overly ambitious schedule, so just approximately from now on:
4. 14 XI: Chapter 3 hopefully completed by Thorsten?
5. (21 XI and/or 28 XI?) Chapter 4: Johannes
6. later Chapter 5 with Hans-Peter
7. Chapter 6: in fact I will be happy to take it, if that’s okay with everybody.