Categories, Proofs and Processes: 20172018
Lecturer 

Degrees 
Schedule C1 (CS&P) — Computer Science and Philosophy Schedule C1 — Computer Science Schedule C1 — Mathematics and Computer Science 
Term 
Michaelmas Term 2017 (20 lectures) 
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 structurepreserving transformations, as mathematical structures in their own right, i.e. categories  which have their own structurepreserving 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 settheoretic 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 settheoretic 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 CurryHoward isomorphism between proofs and programs, and at Linear Logic, a resourcesensitive 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.
Remark: It is recommended that students who intend to write their MSc thesis in the Quantum Group at the Department of Computer Science take this course and additionally the Quantum Computer Science course.
Learning outcomes
 To master the basic concepts and methods of categories.
 To understand how categorytheory 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 CurryHoward 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 CurryHoward correspondence. Introduction to Linear Logic. The connection between logic and categories.
 Further topics in category theory. Algebras and coalgebras. Connections to programming (structural recursion and corecursion).
A. Categories
 Background and definition
 Monics, epics, isomorphisms
 Products and coproducts
 Limits and colimits
 Functors and natural transformations
 Universal arrows and adjunctions
 Cartesian closed categories
B. Connections with logic
 Natural deduction, lambda calculus and CurryHoward isomorphism
 Gentzen sequent calculus and linear logic
 Symmetric monoidal closed categories and categorical semantics of linear logic
C. Further topics
 Algebras
 Coalgebras
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/materials1617/catsproofsprocs/LNPnotes.pdf
The following books provide useful background reading.
 Steve Awodey, Category Theory, 2nd ed., OUP (2010)
 B. C. Pierce, Basic Category Theory for Computer Science, MIT Press (1991)
 F. W. Lawvere and S. H. Schanuel, Conceptual Mathematics, Cambridge University Press (1997)
 S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Springer (1998)
 M. Barr and C. Wells, Category Theory for Computer Science, 2nd ed., Prentice Hall (1995)
 J.Y. Girard, Y. Lafont, and P. Taylor, Proofs and Types,
http://www.paultaylor.eu/stable/prot.pdf
Of these, the book by Pierce (2) provides a very accessible and userfriendly first introduction to the subject (though we will cover more topics in the course).
The book by Awodey (1) is the closest to our course, and an excellent presentation of the subject.