PhD in Extensible Programming Languages for Data Structures in Monoidal Categories

This project will build a bridge between the two strands of theoretical computer science, (a) algorithms and complexity theory and (b) logic and programming language theory, and to put the resulting bridge into practical applications such as in the efficient implementations of mechanized proof assistants.  Algorithm designers have developed a wealth of sophisticated techniques for organising and processing data. In parallel, logicians and programming language theorists have developed linear type systems, which check how computational resources are used, and mathematical interpretations of these systems in structures called monoidal categories.  

The key observation underlying this project is that many existing algorithms can be expressed in suitable linear type systems. Interpreting them in different monoidal categories can therefore yield new algorithms and data structures, allowing established designs to be adapted rather than developed from scratch.  Concretely, the student will design and implement a new functional programming language that at the same time (1) can be extended with linear and non-linear type formers and (2) can be interpreted in user-defined monoidal categories.  These categories can be either defined internally in the language itself or alternatively another proof assistant such as Isabelle. The project will investigate the design space of such a system, including whether to develop a standalone language or embed it within an existing proof assistant.   

A central application will be the efficient implementation of proof assistants based on dependent type theory, such as Lean, Rocq and Agda. For example, interpreting catenable lists (a data structure supporting efficient concatenation) in the monoidal category of endofunctors on types yields a representation of syntax trees with efficient variable substitution.  Substitution is a fundamental operation in type theory, so improving its implementation could reduce the cost of checking proofs.   Expected outcomes include a prototype programming language, mathematical foundations for its interpretation mechanisms, and potentially a more efficient implementation of a proof assistant based on dependent type theory. Together, these outcomes will establish a connection between two traditionally distinct strands of theoretical computer science, yielding practical advances in the development of secure and efficient software. 

Location 

University of Exeter, Streatham Campus

Advert information