Seminar CurryHowardKorrespondenz WS13
Dozenten  Tadeusz Litak und Daniel Gorín 
Ort  Seminarraum LS INF8, Martensstr. 3, 11. OG 
Termine  Thu 18:15 
Umfang  Seminar, 2 SWS, ECTSStudium, ECTSCredits: 5 
Studienfächer / Studienrichtungen  PF INFMA ab 7 (ECTSCredits: 5), PF INFBAS ab 4 (erw. Teiln. 95) (ECTSCredits: 5), PF INFBAW ab 4 (erw. Teiln. 96) (ECTSCredits: 5), WF MBA ab 4 (ECTSCredits: 5), WF MMA ab 7 
What makes proof assistants work?
Apart from the whole tactics business, what is the real difference between Coq and Agda? Why computer scientist should bother with lambda calculi and type systems? Is “CurryHoward correspondence” a bunch of letters between two old guys? Or a fake Indian dish in American restaurants? 
This seminar answer all these questions…
…plus a few others you were too afraid to ask…
…or never thought of asking.
Contents
As the name indicates, we will spend the semester reading papers on CurryHoward 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.
Knowledge and competences
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, MartinLö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.
Proposed reading list
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 9780444520777.
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.
Schedule

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 alphaequivalence classes, then there is a standard technique applied in CS which does not require using too abstract categorical/algebraic apparatus: via socalled de Bruijn indices. And for an alternative introduction to lambda calculus than this first chapter, see these notes of Barendregt and Barendsen.

31 X: We discussed Chapter 2. I distributed another Chapter 2—of Chagrov & Zakharyaschev book on modal logic—as an additional reference.

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:

14 XI: Chapter 3 hopefully completed by Thorsten?

(21 XI and/or 28 XI?) Chapter 4: Johannes

later Chapter 5 with HansPeter

Chapter 6: in fact I will be happy to take it, if that’s okay with everybody.