PhD in Extensible Programming Languages for Data Structures in Monoidal Categories

at University of Exeter, Exeter, United Kingdom

Listed on EduAtlas: live school vacancies from schools’ own careers pages and public job services. Apply on jobs.ac.uk.

Salary

£21,805 a year

Closing date

8 December 2026

Start

Not given in the advert

Type of post

Research

Contract

Full Time, Fixed-Term/Contract

First seen

27 October 2026, on jobs.ac.uk

ApplySave

On jobs.ac.uk · Send it by: WhatsApp · LinkedIn · Email · X

See 10 more vacancies at University of Exeter

Find posts like this from Claude: add EduAtlas to Claude.

The advert

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 £21,805. The studentship will provide funding of fees and a stipend per annum for 2026/7

About University of Exeter

Type

University

Other vacancies at University of Exeter

University of Exeter: full school record · More vacancies in United Kingdom

Linked to this school by its name and place in the advert.