Categories, Proofs and Processes:  2024-2025

Overview

Category Theory is a powerful mathematical formalism which has become an important tool in modern mathematics, logic and computer science. One main idea of Category Theory is to study mathematical `universes', collections of mathematical structures and their structure-preserving transformations, as mathematical structures in their own right, i.e. categories, which again have their own structure-preserving transformations (functors). This is a very powerful perspective, which allows many important structural concepts of mathematics to be studied at the appropriate level of generality, and brings many common underlying structures to light, yielding new connections between apparently different situations. This unifying language allows one, for instance, to give a correspondence between mathematical proofs and computer programs through the Curry-Howard correspondence. Category theory has also deeply influenced the design of modern (especially functional) programming languages, e.g. the concept of the monad was lifted from Category Theory. More recently the tools of Category Theory have been adapted to study probabilistic and quantum processes in the hope of giving a unifying framework in which to study information processing. 

This course will introduce and develop the basic ideas of Category Theory, and explore some of the aforementioned applications to logic, programming and processes. 

Learning outcomes

• To master the basic concepts and methods of categories.

• To understand how category-theory can be used to structure mathematical ideas, with the concepts of functoriality, naturality and universality; and how reasoning with objects and arrows can replace reasoning with sets and elements. To learn the basic ideas of using commutative diagrams and unique existence properties.

• To understand the connections between categories and logic, focussing on the Curry-Howard isomorphism.

• To understand how some basic forms of computational processes can be modelled with categories.

Prerequisites

Some familiarity with basic discrete mathematics: sets, functions, relations, mathematical induction. Basic familiarity with linear algebra and logic: propositional and predicate calculus. Some familiarity with programming, particularly functional programming, would be useful but is not essential.

Synopsis

The course content will be structured as below, where we start with an introduction to Category Theory in generality and move on to particular categories of interest. 

• Introduction to Category Theory:
  • Categories
  • Functors
  • Natural transformations
  • Universality and Adjoints
  • Monads
• Cartesian closed categories:
  • Curry-Howard correspondence
• Monoidal categories:
  • Markov categories

Reading list

Slides will be provided on the course material page. The standard reference is

•     Abramsky and Tzevelekos, "Introduction to Categories and Categorical Logic",
      https://www.cs.ox.ac.uk/teaching/materials16-17/catsproofsprocs/LNPnotes.pdf

The following books provide useful background reading.

1.     Steve Awodey, Category Theory, 2nd ed., OUP (2010)
2.     B. C. Pierce, Basic Category Theory for Computer Science, MIT Press (1991)
3.     S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Springer (1998)
4.     B. Milewski. Category Theory for Programmers. https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.