Course Outline

Instructor: Michael Winter, Office J323, Office J323, Office Hours: Tue 1:00pm-3:00pm & Wed, 9:00am - 11:00am, email:

Calendar description

Introduction to typed and untyped lambda calculi and their semantics. Syntax of the lambda calculus, conversion, fixed points, reduction, Church-Rosser theorem, representation of recursive functions, lambda models. Category theory, cartesian closed categories and categorical models of lambda calculus.

Course Outline

Date Topics
1 Jan 06/08 Introduction, Simply typed λ-calculus with explicit pairs
2 Jan 13/15 Simply typed λ-calculus with explicit pairs, Confluence (Church-Rosser)
3 Jan 20/22 Categories, Morphisms
4 Jan 27/29 Constructions, Cartesian closed categories (Test 1)
5 Feb 03/05 Constructions, Functors and Adjunctions
6 Feb 10/12 Categorical semantics of the simply typed λ-calculus
7* Feb 24/26 Variant types and recursion
8 Mar 03/05 Untyped λ-calculus (Test 2)
9 Mar 10/12 Recursive Domain Equations
10 Mar 17/19 Recursive Domain Equations (continued)
11 Mar 24/26 Algebras, primitive recursion and catamorphisms (Test 3)
12 Mar 31/Apr 02 Second order λ-calculus, Review
* Feb 16-20 is Reading Week, no classes.


COSC Home Page
COSC 5P05 Home Page
© M. Winter, 2015