COSC 5P05 Course Outline

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

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

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

Texts

• The main text book: Categories, Types, and Structures
• Additional Material on the lambda calculus: Lambda Calculus
• H. Barendregt: Lambda Calculi with Types