Computer Laboratory

Course pages 2013–14

Category Theory and Logic

Principal lecturers: Prof Glynn Winskel, Dr Jonas Frey
Taken by: MPhil ACS, Part III
Code: L108
Hours: 16
Prerequisites: Basic familiarity with logic and set theory (e.g. Discrete Mathematics I and II from Part 1A Computer Science course), with the lambda calculus (e.g. Part 1A Foundations of Computer Science) and with inductively-defined type systems (e.g. Part 1B course on Semantics of Programming Languages)


Category theory is a framework for organizing kinds of mathematical structure. In this course we will use category theory to organize and develop the kinds of structure that arise in models and semantics for logics and programming languages.


  • Categories. Basic definitions and examples.
  • Products. Categorical semantics for a simple calculus with pairing and projection.
  • Typed lambda calculus, cartesian closed categories, and intuitionistic propositional logic.
  • Functor categories and presheaf categories.
  • Quantifier-free predicate logic: monomorphisms and pullbacks.
  • Slice categories. Proof-relevant interpretation of predicate logic.
  • Adjunctions, monads.
  • The existential quantifier as a left adjoint.


On completion of this module, students should:

  • be familiar with the basic definitions of category theory; and
  • be able to interpret logic, proof and programs in categories with appropriate structure.


The coursework in this module will consist of a graded exercise sheet.


Assessment will consists of:

  • a graded exercise sheet (25% of the final mark), and
  • a take-home test (75%).

Recommended reading

Crole, R. L. (1994). Categories for types. Cambridge University Press.
Awodey, S. (2010). Category theory. Oxford University Press (2nd ed.).