As a recipient of the Denotational semantics via (2-dimensional) categories studentship, you will receive: 

The project will be in the field of denotational semantics, a branch of theoretical computer science in which one builds mathematical models of programming languages. Such models are used in many ways. For example, might answer questions about program behaviour: one can show that no program exists with a certain behaviour, or understand how programs with complex collections of features -- such as probability, looping, and exceptions -- ought to behave. Alternatively, by studying models of programs we can understand the mathematical structure of programs, and thereby discover new language paradigms or constructs.  

Just as physics draws on mathematics, and can lead to mathematical results in its own right, so denotational semantics often intersects with deep and interesting mathematical ideas. The project will use the powerful language of category theory to build new models and study the relationships between existing ones. In particular, it will likely make use of 2-dimensional category theory and category-theoretic universal algebra. 2-dimensional categories have more data than categories, which means they can be used to construct models which reflect more refined relationships between programs. Moreover, 2-dimensional categories are a natural way to describe common structures on categories, and hence on models. Universal algebra, on the other hand, is a branch of logic studying the structures formed by collections of operations and equations. For computer science, this gives us a way to think about many different programming languages simultaneously, by thinking of them as determined by a choice of basic operators and relations between them. 

Three potential areas for inquiry are below. The list is not exhaustive, and I am happy to tailor a topic to the successful applicant. Potential students may also, if they wish, propose their own ideas for projects. 

1. Developing the theory of the strong pseudomonads. In LICS 24 Hugo Paquet and I introduced strong pseudomonads as a 2-dimensional counterpart of the strong monads used to model effectful programs (as in Haskell, for example). However, much of their theory remains to be explored: this would be the starting point for the PhD project. Possible aspects include:  

(a) their type-theoretic internal language, and links between coherence and strong normalisation for this language; 

(b) examples of models which make explicit why programs can be re-ordered; 

(c) connections to multi-ary models of type theory. 

2. Closed categories and combinators. Despite their very different roots, there seems to be a connection between closed categories, which axiomatise the structure of collections of functions, and combinatory logic, which is a binding-free language closely related to the lambda calculus. I briefly explored this idea in a recent paper (FoSSaCS 24). This project would extend that by finding other examples of connections between closed-like structures and combinatory logic, and trying to understand the underlying general theory of these connections.  

3. Multi-ary models of programming languages. A category abstracts away from the behaviour of sets and functions, so its arrows have one input and one output. Programs, however, typically have multiple inputs: this is captured by multicategories. Because of their tight correspondence with syntax, multicategories form an often-overlooked bridge between syntax and categorical semantics. This idea has recently been exploited for simple type theories: the project would explore using ideas from enriched category theory and 2-category theory to extend this to programming languages. Possibilities include: 

(a) adding constructs such as recursion or side-effects, 

(b) capturing algebraically languages in which programs are related in fine-grained ways, such as by using a metric distance to give a fuzzy notion of program sameness.

This scholarship is available to UK and international applicants. 

Applicants are typically expected to hold an upper second-class (2:1) undergraduate honours degree (or equivalent qualification) in a related field. However, those who do not meet this requirement may still be considered if they hold a relevant postgraduate qualification or can demonstrate sufficient professional experience to compensate. 

The University of Sussex believes that the diversity of its staff and student community isfundamental to creative thinking, pedagogic innovation, intellectual challenge, and theinterdisciplinary approach to research and learning. We celebrate and promote diversity,equality and inclusion amongst our staff and students. As such, we welcome applicants from allbackgrounds. 

Please ensure you application includes the following: