Time and Location: MWF 9:30-10:30, Chase 319.

Instructor: Peter Selinger. Office: Chase 303. Email: selinger@mathstat.dal.ca (please mention "4680" or "5680" in the subject line). Phone: 494-3311.

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.

[1] is a standard reference handbook on the lambda calculus. [2]-[4] are textbooks on the lambda calculus. [5]-[7] are textbooks on the semantics of programming languages. Finally, [8]-[9] 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 [1]-[3] are more mathematically oriented, whereas [4]-[9] are more oriented towards computer science.

• [1] H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North-Holland, 2nd edition, 1984.
• [2] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.
• [3] J.-L. Krivine. Lambda-Calculus, Types and Models. Masson, 1993.
• [4] G. E. Révész. Lambda-Calculus, Combinators and Functional Programming. Cambridge University Press, 1988.
• [5] G. Winskel. The Formal Semantics of Programming Languages. An Introduction. MIT Press, London, 1993.
• [6] J. C. Mitchell. Foundations for Programming Languages. MIT Press, London, 1996.
• [7] C. A. Gunter. Semantics of Programming Languages. MIT Press, 1992.
• [8] S. L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987.
• [9] A. W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

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: 90–100 = A+, 85–89.9 = A, 80–84.9 = A–, 75–79.9 = B+, 70–74.9 = B, 65–69.9 = B–, 62–64.9 = C+, 58–61.9 = C, 55–57.9 = C–, 50–54.9 = D, 0–49.9 = F.

Course Homepage: Updated information, homework sets, lecture notes, handouts, etc., will be available from http://www.mathstat.dal.ca/~selinger/5680/

To Peter Selinger's Homepage: