I am a researcher in formal verification (as of Nov 2025) at Zeroth Research, a focused research organization funded by the UK government’s Advanced Research + Invention Agency through its Safeguarded AI programme. My work at Zeroth is on interfacing SMT solvers with type-theoretic proof assistants to enable automated proof search.
Previously, I was a PhD student in the Theory of Computation group at the University of Birmingham. I completed my PhD in June 2025 under the supervision of Martín Escardó, and with Vincent Rahli as my second supervisor.
Before I started my PhD, I obtained an MSc degree from Chalmers University of Technology. For my MSc thesis there, I investigated formal topology in the context of univalent type theory, under the supervision of Thierry Coquand.
Most of my PhD work was focused on making predicative sense of constructive point-free topology in the constructive and predicative context of univalent type theory. Throughout my PhD, my supervisor and I have carried out a constructive and predicative development of locale theory in univalent foundations, with a particular focus on the theory of spectral and Stone locales (including Stone duality) and the point-free topology of domains. This work is related to, but different from, formal topology, which has historically been the standard way to develop point-free topology predicatively in type theory.
More broadly, my primary research interest is the connection between topology and computation. Domains and topology are an indispensable tool for approaching this connection, but I am interested in other such tools such as synthetic topology.