Time and Location: MWF 9:30-10:30, Chase 319.
Instructor: Peter Selinger. Office:
Office Hours: MW 1-2.
Course Description: This course covers topics of current interest in logic and/or the foundations of computation. This year, we will study the lambda calculus, a mathematical tool that is used in logic, computability theory, and the study of programming languages. The lambda calculus was invented in the 1930's by Church and Curry as part of their approach to the foundations of mathematics. On the one hand, it can be regarded as an idealized programming language. On the other hand, it can be regarded as a notation for writing mathematical proofs. This connection between proofs and programs, known as the Curry-Howard isomorphism, gives a very powerful way and flexible way of relating mathematics and computer science.
Topics: Typed and untyped lambda calculi, foundations of functional programming languages, Curry-Howard isomorphism, normalization and rewriting theory, evaluation strategies, operational semantics, denotational semantics, and categorical semantics, type assignment, polymorphism, fixed-point programming, abstract machines.
Prerequisites: MATH 3030X/Y.06 or MATH 3500X/Y.06, or CSCI 3110.03 and CSCI 3136.03, or consent of the instructor.
This course is suitable for advanced undergraduates as well as graduate students, from both mathematics and computer science. Suggested prerequisites for math students are algebra and analysis at honours undergraduate level. Students from computer science should be familiar with formal language theory and concepts of programming languages. All students should be comfortable with writing mathematical proofs. When in doubt about prerequisites, please consult the instructor.
Lecture Notes: P. Selinger, "Lecture Notes on the Lambda Calculus", available from http://arxiv.org/abs/0804.3434.
Reading Materials: The following is a list of some textbooks and other books on the lambda calculus. None of them are required reading for the course, but you may nevertheless find it interesting or helpful to browse them. I will ask to put them on reserve in the library, to the extent that they are available.
 is a standard reference handbook on the lambda calculus. - are textbooks on the lambda calculus. - are textbooks on the semantics of programming languages. Finally, - are textbooks on writing compilers for functional programming languages, but they contain a wealth of material on the lambda calculus in a more practical context. The books - are more mathematically oriented, whereas - are more oriented towards computer science.
Course Work: There will be an in-class midterm and a final exam. There will be weekly or biweekly homework assigned in class. Graduate students will be given additional homework and/or additional exam questions. Graduate students will also be expected to give an in-class presentation towards the end of the term. For undergraduate students, this additional work is optional and voluntary.
Grading: Grades will be based on the exams, homework, and
presentations (if applicable). Active participation in class may be
taken into account. You must pass the final exam to pass the course.
Grades will be calculated as follows: homework 10–20%, midterm
20–40%, final exam 40–70%, presentations 10–20% (for
graduate students) or 0–20% (for undergraduate students). Within
these constraints, and provided they add up to 100%, you may pick your
own percentages. Numerical grades are converted to letter grades via
the standard Faculty of Science scheme:
Updated information, homework sets, lecture notes, handouts, etc.,
will be available from
To Peter Selinger's Homepage: