Every time a smartphone app crashes or a self-checkout till freezes, the culprit is often a mismatch between how programmers think their code should behave and how the computer actually runs it. This project aims to fix that mismatch by building cleaner mathematical models for "computational effects"—the messy, real-world behaviours like reading memory, handling errors, or making random choices that make programs unpredictable. The problem is that existing mathematical frameworks for describing these effects are needlessly complicated and rigid. They cannot easily handle combinations of effects—say, a program that both reads from overlapping memory regions and throws exceptions—nor can they track how much memory or time a piece of code uses. This project uses category theory, a branch of abstract mathematics, to design simpler, more flexible models that do both. This is fundamental science. It will not directly produce a new app or a faster processor. But by giving programming-language designers a cleaner conceptual toolbox, it could lead to compilers that catch more bugs automatically, languages that are easier to reason about, and ultimately software that fails less often. Past work in this area has already shaped how modern functional languages like Haskell handle side effects; this project aims to extend that success to stateful, pointer-heavy code that underpins operating systems and databases.
View original technical description
This project develops new algebraic structures for programming language semantics. It is concerned with common software features such as effects, functions, state, interference, modularity, pointer manipulation, iteration, types and polymorphism. It uses category theory (a branch of mathematics) to provide suitable modelling frameworks. The research area stems from the traditional classification of programming languages into "functional", where a program represents a function, and "imperative". where a program instructs the computer. These are combined into "programming with effects", where an "effect" is a behaviour such as reading and writing to memory, performing input and output, or making nondeterministic choices. To ensure the correctness of such software, a clear understanding of the algebraic structure is essential. To this end, we consider each effect individually, and also combinations of effects, as well as the interplay between effects and the functional parts of a program. The problem is that the structures proposed in the past seem to be unnecessarily complicated, specialised and rigid. So this project aims to develop models that are simpler and more flexible, in several ways, taking advantage of recent mathematical developments. To begin, we adapt the existing modelling of functional programming with effects so as to simplify the calculations that it requires. Furthermore, we aim to allow models that track resource usage, which the existing framework excludes. We then develop the step-by-step construction of algebraic structures for combined effects to make it compatible with stateful operations (the existing account is not). We then investigate the combination of stateful operations (reading and writing memory) for memory regions that are separate or even overlapping. The biggest challenge here is dealing with memory consisting of multiple regions that overlap in complex ways; we must ensure that the equations governing the overlap between each pair of regions correctly determine the behaviour of the whole memory. Furthermore, by generalising the framework in which this analysis takes place, our results should extend to effects other than state, such as exception handling. The next part confronts a different kind of challenge relating to stateful effects: modelling programs that combine iteration with pointer manipulation and dynamic allocation of memory cells. Although such software is widespread, the challenge is to interpret it in a way that is concrete (it allows explicit calculation) and yet abstract (it assigns the same meaning to pieces of code that cannot be distinguished by an external test). The resulting computational modelling framework will serve as a foundation for studying more advanced languages. Although types play a large role throughout this project, they are central to the last part. Here we look at types for "polymorphic" programs that can be applied to arguments of different type. We consider when such types are essentially the same, so that a program written for one such type can be automatically converted into a program for another. We plan to obtain at least a substantial list of cases where this happens, and hopefully even a complete list. By simplifying and elaborating the algebraic structure of effectful programs, this project will provide a toolbox of concepts and results to benefit researchers in semantics, and in the longer term, programmers and language designers and implementors.
Plain English summaries and category classifications on this site are generated by AI and may not perfectly reflect the original research.
Is something wrong? Let us know