Computer Laboratory

Course pages 2011–12

Category Theory and Logic

Principal lecturer: Dr Sam Staton
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 implication.
  • The category of arrows and the validity/invalidity of Peirce's law.
  • Quantifier-free predicate logic: monomorphisms and pullbacks.
  • Slice categories. Proof-relevant interpretation of predicate logic.
  • 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 comprise assessed exercises using the Agda programming language.


Assessment will be 25% by coursework, and 75% by a take-home exam.

Recommended reading

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