Lecturer

Nikos Tzevelekos

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 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.

Another important aspect is that set-theoretic reasoning with elements is replaced by reasoning in terms of arrows. This is more general, more robust, and reveals more about the intrinsic structure underlying particular set-theoretic representations.

Category theory has many important connections to logic. We shall in particular show how it illuminates the study of formal proofs as mathematical objects in their own right. This will involve looking at the Curry-Howard isomorphism between proofs and programs, and at Linear Logic, a resource-sensitive logic. Both of these topics have many important applications in Computer Science.

Category theory has also deeply influenced the design of modern (especially functional) programming languages, and the study of program transformations. One exciting recent development we will look at will be the development of the idea of coalgebra, which allows the formulation of a notion of coinduction, dual to that of mathematical induction, which provides powerful principles for defining and reasoning about infinite objects.

This course will develop the basic ideas of Category Theory, and explore its applications to the study of proofs in logic, and to the algebraic structure of programs and programming languages.

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 structural proof theory and 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 logic: propositional and predicate calculus. Some first acquaintance with abstract algebra: vector spaces and linear maps, and/or groups and group homomorphisms. Some familiarity with programming, particularly functional programming, would be useful but is not essential.

Synopsis

• Introduction to category theory. Categories, functors, natural transformations. Isomorphisms. monics and epics. Products and coproducts. Universal constructions. Cartesian closed categories. Symmetric monoidal closed categories. The ideas will be illustrated with many examples, from both mathematics and Computer Science.
• Introduction to structural proof theory. Natural deduction, simply typed lambda calculus, the Curry-Howard correspondence. Introduction to Linear Logic. The connection between logic and categories.
• Further topics in category theory. Algebras, coalgebras and monads. Connections to programming (structural recursion and corecursion), and to programming languages (monads as types for computational effects).

Categories: 10 lectures.
1 each for the following topics:
Categories
Monics, epics, isomorphisms
Products and coproducts
Limits and colimits
Functors and natural transformations
Universal arrows
Adjunctions
Monads
Cartrsian closed categories
Symmetric monoidal closed categories
Connection to Logic: 4 lectures
Algebras and coalgebras: 4 lectures.

Reading list

• Basic Category Theory for Computer Science, Pierce.
• Conceptual Mathematics, Lawvere and Schanuel.
• Categories for the Working Mathematician, Saunders Mac Lane.
• Categories and Types, R. Crole.
• Proofs and Types, Girard, Lafont and Taylor.
• Algebra of Programming, Bird and de Moor.

Of these, the book by Pierce provides a very accessible and user-friendly first introduction to the subject.

Feedback

Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.

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.