Place: BH 150

Time: M 3:30 - 5:50

Instructor: Steve Awodey

Office: Baker 152 (mail: Baker 135)

Office Hour: Monday 1-2, or by appointment

Phone: 8947

Email: awodey@andrew

Secretary: Baker 135## 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 intuitionistic logic.

Overview## 80-413/713 Category Theory, or equivalent.

Prerequisites

Topics will be selected from the following

- Functorial semantics for algebraic theories
- Simple type theory and cartesian closed categories
- Dependent type theory and locally cartesian closed categories
- Functorial semantics for elementary logic
- Higher-order logic
- Basic topos theory
- Sheaf semantics
- Algebraic set theory

TextsRecommended

- 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.
- Johnstone, P.: Sketches of an Elephant. Cambridge, forthcoming.

Supplemental

- 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.
- 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.
## Grades will be based on occasional homework problem sets for undergraduates.

Requirements and Evaluation

Graduate students are required to also prepare and present one lecture on a topic provided by the instructor.

Undergrads have the option of lecturing or taking a final exam.

Course materialsLecture notes:Lecture notes are here.