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 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. e.g. treating the lambda-calculus via the theory of cartesian closed categories.
Higher-order logic is treated categorically by the theory of topoi.
We shall see how this idea connects logic with topology (the models of a theory form a space).

A prerequisite for this course is familiarity with basic category theory (as treated in the course 80-413/713).

*Contact me for any questions, particularly if you are unsure the course is for you.*