Course on the second order lambda-calculus

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:


The course will give an introduction to the second order lambda-calculus with focus on some of the following topics:


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.

Sign up

To sign up for the course, please contact Rasmus Møgelberg.


At this point, the following students have signed up for the course:

Time and place

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.

Course material

Supplementary Material

The following articles may also be of interest