Syntax and semantics of 2-dimensional type theories

This project seeks to create a new and powerful interplay between theoretical computer science and pure mathematics. More precisely, we will investigate a class of formal systems known as 2-dimensional type theories, which allow us to express in a direct way the steps that take place in real-world computations by having a primitive notion of rewriting.

Our goal is to transform the state of the art in this area by providing a comprehensive theory of these systems and their mathematical models. Importantly, we will develop our study of models both in general, abstract terms (so as to encompass simultaneously as many theories as possible) as in concrete examples. In particular, we will develop further the theory of 2-dimensional categories.

We also seek to obtain models for 2-dimensional type theories with ideas coming from two of the most active and exciting areas of pure mathematics at present: higher-dimensional algebra and categorification, in which one is concerned with replacing ordinary set-based structures with subtler ones, so as to obtain more powerful invariants.