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:
- 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.
Description
The course will give an introduction to the second order
lambda-calculus with focus on some of the following topics:
- Strong normalisation
- Encoding inductive datatypes
- Parametricity and consequences
- The PER-model
Prerequisites
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.
Teachers
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.
Participants
At this point, the following students have signed up for the course:
- Nina Bohr
- Christian Stefansen
- Troels C. Damgaard
- Noah Torp-Smith
- Rasmus Lerchedahl Petersen
- Syed Imran Abrar Hussain
- Bodil Biering
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
Lunch
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
- 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
Supplementary Material
The following articles may also be of interest