Computer Laboratory

Course pages 2014–15

Category Theory and Logic

Principal lecturer: Prof Andrew Pitts
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)

Aims

Category theory provides a unified treatment of mathematical properties and constructions that can be expressed in terms of "morphisms" between structures. It gives a precise framework for comparing one branch of mathematics (organized as a category) with another and for the transfer of problems in one area to another. Since its origins in the 1940s motivated by connections between algebra and geometry, category theory has been applied to diverse fields, including computer science, logic and linguistics. This course introduces the basic notions of category theory: category, functor, natural tansformation and adjunction. We will use category theory to organize and develop the kinds of structure that arise in semantics for logics and programming languages.

Syllabus

  • Categories. Basic definitions and examples. Duality.
  • Products. Categorical semantics of equational logic.
  • Typed lambda calculus, cartesian closed categories, and intuitionistic propositional logic.
  • Naturality. Functor categories and presheaf categories. The Yoneda Lemma.
  • Quantifier-free predicate logic: monomorphisms and pullbacks.
  • Adjunctions. Quantifiers as adjoints. Locally cartesian closed categories and Type Theory.

Objectives

On completion of this module, students should:

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

Coursework

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

Assessment

Assessment will consists of:

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

Recommended reading

Awodey, S. (2010). Category theory. Oxford University Press (2nd ed.).

Crole, R. L. (1994). Categories for types. Cambridge University Press.

Pitts, A. M. (2000). Categorical Logic. Chapter 2 of S. Abramsky, D. M. Gabbay and T. S. E. Maibaum (Eds) Handbook of Logic in Computer Science, Volume 5. Oxford University Press. (Draft copy available here.)