Categories, Proofs and Programs

---

BA in Computer Science BA in Mathematics & Computer Science MSc in Computer Science MSc in Mathematics and the Foundations of Computer Science

16 lectures MT Professor Samson Abramsky

---

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.

---