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
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 intuitionistic logic.
Prerequisites
80-413/713 Category Theory, or equivalent.
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
Texts
Recommended
- 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.
Requirements and Evaluation
Grades will be based on occasional homework problem sets for undergraduates.
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 materials
Lecture notes: Lecture notes are here.
Steve
Awodey
awodey@cmu.edu