Math 4680/5680,
Topics in Logic and Computation
Fall 2007 Peter Selinger |

Updates are shown in red.

**Time and Location:** TTh 11:30-1, Chase 319.

Please note that there will be **no class on September 11 and 13,**
because I will be away at a conference. These two classes will be made
up later in the term. The first class is on September 6, and the
second class is on September 18.

**Instructor:** Peter Selinger. Office:

**Office Hours:** TBA.

**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
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
and denotational 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.

**Textbook:** None. There will be handouts.

**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.

**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:

selinger@mathstat.dal.ca / PGP key