Place: BH 150
Time: TR 12 - 1:20
Instructor: Steve Awodey
Office: Baker 135F
Office Hour: Thursday 1-2, or by appointment
OverviewThis 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.
Prerequisites80-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
- Functorial semantics for algebraic theories
- Functorial semantics for elementary logic
- Higher-order logic and basic topos theory
- Sheaf semantics and Grothendieck toposes
- Simple type theory and cartesian closed categories
- Dependent type theory and locally cartesian closed categories
- Homotopy type theory
- Steve Awodey, Category Theory, 2nd edition, Oxford University Press, 2010.
- Crole, R. L.: Categories for Types. Cambridge University Press, Cambridge, 1993.
- Lambek, J. and Scott, P.: Introduction to Higher-Order Categorical Logic. Cambridge University Press, Cambridge, 1986.
- Mac Lane, S. and Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, 1992.
- Asperti, A. and Longo, G.: Categories, Types, and Structures. MIT Press, 1991.
- Barr, M. and Wells, C.: Categories for Computing Science, 3rd edition.
- Borceux, F.: Handbook of Categorical Algebra (Encyclopedia of Mathematics and its Applications). Cambridge University Press, 1994.
- Freyd, P.\ and Scedrov, A.: Categories, Allegories. North-Holland, 1995.
- Johnstone, P.: Sketches of an Elephant. Cambridge University Press.
- Makkai, M.\ and Reyes, G.: First-Order Categorical Logic. LNM 611, Springer, 1977.
- Mac Lane, S.: Categories for the Working Mathematician. Springer, 1971. (the standard reference)
- McLarty, C.: Elementary Categories, Elementary Toposes. Oxford Logic Guides 21, Oxford University Press, 1992.
Requirements and EvaluationGrades will be based on 5-6 homework problem sets and a presentation with a brief written report.
Course materialsLecture notes: Lecture notes will be posted here.
Homework: Problem sets will be posted here.