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

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

[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