Monday 14 February 2022

MGS 2022: String diagrams for monoidal closed categories

Between 10-13 April 2022 I will teach an advanced course at the Midlands Graduate School, on the topic of string diagrams for monoidal closed categories. 

String diagrams are a graphical formalism for category theory which found recent widespread applications in areas as diverse as quantum computing or computational linguistics. These languages are based on compact-closed categories, a mathematical framework that generalises the concept of relations. 

In contrast, programming languages are based on monoidal-closed categories, a mathematical framework that generalises the concept of function spaces. String diagrams for these categories have been studied less, yet they are useful in bridging the gap between the syntax of programming languages and and the principled extraction (or distillation) of efficient abstract machines. They are also useful in clarifying complex syntactic transformations such as closure conversion or automatic differentiation. 

The attending student will be assumed to have some familiarity with basic category theory. Understanding of compilers is not required but it will provide additional motivation. 

Understanding the issue of equality in Homotopy Type Theory (HoTT) is easier if you are a programmer

We programmers know something that mathematicians don't really appreciate: equality is a tricky concept. Lets illustrate this with a str...