Categorical Logic

80-514/814

Fall 2019

Course Information

Place: BH 150
Time: TR 12 - 1:20
Instructor: Steve Awodey
Office: Baker 135F
Office Hour: Tuesday 2-3, or by appointment
Email: awodey@andrew

Overview

This course focuses on applications of category theory in logic and computer science. A leading idea is functorial semantics, according to which a model of a logical theory is a set-valued functor on a structured category determined by the theory. This gives rise to a syntax-invariant notion of a theory and introduces many algebraic methods into logic, leading naturally to the universal and other general models that distinguish functorial from classical semantics. Such categorical models occur, for example, in denotational semantics. In this connection the lambda-calculus is treated via the theory of cartesian closed categories. Similarly higher-order logic is modelled by the categorical notion of a topos. Using sheaves, topos theory also subsumes Kripke semantics for modal and intuitionistic logics. Locally cartesian closed categories provide semantics for dependent type theories. Time permitting, we will consider Martin-L"of type theory and the recent extension of it to Homotopy type theory.

Prerequisites

80-413/713 Category Theory, or equivalent. A prerequesite for this course is familiarity with basic category theory, but depending on demand the course can start with a quick refresher of the central concepts.
CS grad students may start after Sept. 9 with consent of instructor.

Topics to be covered

Texts

Recommended Supplemental

Requirements and Evaluation

Grades will be based on 5-6 homework problem sets, and for grad students, a presentation with a brief written report.

Course materials

Lecture notes: Lecture notes will be posted here, in the files catlogX.
Homework: Problem sets will be posted here, in the file catloghw.


Steve Awodey
awodey@cmu.edu