Success for Oxford computer scientists at POPL 2025

Three papers authored by members of the department were featured at POPL 2025, the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages.  

POPL is the premier forum for foundational innovations in the design, definition, analysis, transformation, and implementation of programming languages, programming systems, and programming abstractions. 

DPhil student Jack Liell-Cock and his supervisor Sam Staton, Professor of Computer Science, presented their paper ‘Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories’  

This paper develops a new mathematical framework that allows different kinds of uncertainty to be combined in a structured way. Existing methods use convex sets of probability distributions, meaning they consider multiple possible distributions at once. However, these approaches rely on monads - abstract mathematical structures used in programming and category theory - that do not combine neatly, making them less flexible. 

The authors solve this by introducing a new approach that explicitly names uncertain choices and manages them using graded monads, a refined version of monads that track additional information. This makes the model fully compositional, meaning probability distributions can be combined in a structured, consistent way. Their model is maximal, meaning it captures as much useful information as possible, and it provides tighter bounds on uncertainty, allowing for more precise reasoning about unknowns.  

This improved framework for handling imprecise probability could enhance machine learning, decision-making under uncertainty, and robust statistical modelling, where accurately managing multiple possible outcomes is crucial for reliability and performance. 

Probabilistic programming languages are widely used for statistical modelling, and we're excited to see whether this new approach can be practically useful for statistical modelling that is more robust, by including imprecise probabilities. This work forms a starting point for our recent ARIA grant, Categorical Probability Towards Safe AI. Professor Sam Staton 

Fourth year student Thien Udomsrirungruang and Strachey Professor of Computing Nobuko Yoshida presented their paper ‘Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types’. This paper was extended from Thien’s Project B as part of his third year optional individual project.

This paper compares two key approaches to Multiparty Session Types (MPST), a method for ensuring safe communication between multiple interacting processes. The top-down approach starts with a global type, a high-level plan of how participants should interact, and checks each process against this plan. The bottom-up approach infers communication rules from individual participants and ensures the whole system follows them.  

Using type graphs, the authors develop new algorithms for checking subtypes (ensuring one type can replace another), type inference (automatically determining communication rules), and property verification. Their analysis shows that top-down is generally more efficient, while bottom-up is computationally expensive, particularly for checking liveness (whether processes can always continue communication). These findings are useful in designing reliable distributed systems, such as cloud computing, financial transactions, or multi-agent systems, where safe and efficient communication between different components is crucial to prevent errors and deadlocks.

Multiparty Session Types are known as a practical type framework which has been applied to different concurrent and distributed programming languages, models and systems. This work made it clear complexity of various verification methods of multiparty session types, answering several open questions in session types. This work is expanded from Thien’s MSC Project B and it was my pleasure to supervise his project. Strachey Professor of Computing Nobuko Yoshida

Alumnus Fabian Zaiser presented a paper alongside his supervisors Andrzej Murawski, Professor of Computer Science, and Luke Ong, formerly Professor of Computer Science, entitled ‘Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops’. This paper received the Distinguished Paper Award, one of seven selected out of 79 accepted papers. 

This research improves how we estimate probabilities in uncertain situations, especially in computer programs that use randomness and loops. These are common in AI, robotics, finance, and healthcare, where decisions depend on probabilities. Existing methods either rely on human-provided hints or use sampling techniques, which can be unreliable. This study introduces two fully automated ways to calculate upper and lower bounds for these probabilities, making them more accurate and trustworthy.  

Residual Mass Semantics estimates an upper bound by looking at how much probability is still left after running a loop many times. It provides a simple and efficient way to approximate the true probability while guaranteeing safety. Geometric Bound Semantics is a more advanced method which models loops using eventually geometric distributions, meaning the probability decreases in a predictable pattern. It uses contraction invariants, which help automatically find formulas that describe how loops behave. 

The study also presents Diabolo, a tool that applies these methods to real-world problems, proving they work across different scenarios. These techniques are particularly useful in safety-critical applications, where knowing the worst-case or best-case probabilities is essential for making reliable decisions. 

I am honoured to receive the Distinguished Paper Award at POPL, together with my former DPhil supervisors Andrzej Murawski and Luke Ong. This project was especially exciting to me because it brings together several interesting mathematical ideas. Translating these theoretical insights into practical results was a lot of hard work and the award is a gratifying confirmation that these efforts were worth it. This work also forms the culmination of my DPhil thesis, so it is particularly rewarding to see the community appreciate its contribution and recognise the broader significance of program analysis for probabilistic programming and Bayesian inference.  Alumnus Fabian Zaiser 

Editor's note: This article was amended on 21 Feb 2025.