The second order lambda-calculus was developed by Girard (1971) and reinvented by Reynolds (1974). Girard invented the calculus in his study of logic, but the viewpoint we will take in this course is that of Reynolds, in which the second order lambda-calculus is a simple functional programming language with polymorphism. Because of its simplicity the calculus provides a good environment for a theoretical study of polymorphism.

The course on second order lambda-calculus will be an advanced course held at the IT University December 2003. It will be held as an intensive one-week course in the second week of the project period (1-5 Dec).

There will be two ways of receiving credit:

- Students may attend the course and hand in a report/ exercises afterwards to receive 7.5 ECTS. The report/exercises should correspond to two weeks of full time studies done after the course. This option is open to all students.
- Students may actively attend the course and receive 2.5 ECTS. This option is for phd-students only.

- Strong normalisation
- Encoding inductive datatypes
- Parametricity and consequences
- The PER-model

The student should have some basic knowledge of programming languages (knowledge of the simply typed lambda-calculus is good, but not necessary). The student should also have some basic mathematical experience, such that he can understand mathematical proofs and construct simple proofs.

The course is open for masters students as well as phd-students, and is not restricted to students from ITU. However, people who are not related to a university should note, that they will be charged 1000 kr pr ECTS for the course.

The course will be taught by Rasmus Møgelberg and Lars Birkedal.

- Nina Bohr
- Christian Stefansen
- Troels C. Damgaard
- Noah Torp-Smith
- Rasmus Lerchedahl Petersen
- Syed Imran Abrar Hussain
- Bodil Biering

We will meet in room 1.03 (at the ITU of course) from 9-12 on all days Dec. 1 to Dec 5

The ph.d.-study board has kindly offered lunch for all participants in the ITU canteen every day of the course from 12-13.

- We will primarily use the book "Proofs and Types" by Girard, translated by Taylor and Lafont. This book is available for download here. We shal concentrate on sections 3.1, 4.1 and chapters 6, 11, 14
- For the parametricity part, we will use (parts of!) a technical report "On the definition of parametricity" by the course responsibles. The report can be found here
- The material that we will be using from "On the definition of parametricity" can to some extend also be found in "A Logic for Parametric Polymorphism" by Abadi and Plotkin. This can be found on Plotkins homepage

- Mitchell and Plotkin: "Abstract types have existensial type"
- John Reynolds: "Towards a theory of type structure", "An introduction to the polymorphic lambda calculus", "Types, abstraction and parametric polymorphism"
- Mitchell: "On the equivalence of data representations"
- Longo and Moggi:"Constructive Natural Deduction and its `&Omega -set' Interpretation"
- Phoa: "An Introduction to Fibrations, Topos Theory, the Effective Topos and Modest Sets"
- B. Jacobs: "Categorical Logic and Type Theory" (Book)
- Longleys Ph.D. thesis: "Realizability toposes and language semantics"
- Two reports by Rasmus Lerchedahl Petersen and Jacob Thamsborg are available here
- Bierman, Pitts, Russo: "Operational semantics of Lily, a polymorphic linear lambda calculus with recursion"