Current Research

Recently, I have been working on both semantics and applications of probabilistic programming. In particular, I am interested in combining probabilistic modelling with traditional programming language constructs and developing reliable inference methods. This poses a significant challenge as traditional measure theory does not suffice as a semantic basis for probabilistic programming languages with higher-order functions and continuous distributions. Recently, my colleagues and I have shown that quasi Borel spaces do form a suitable semantic basis for proving the correctness of inference algorithms for such expressive probabilistic programming languages. More recently, with Luke Ong, I have been developing a game semantics to provide the first fully abstract semantics for probabilistic programming with continuous distributions as well as the first semantics for imperative higher-order continuous distributions probabilistic programming languages.

On the more applied side, I am a member of Stan language team and have recently been contributing to improve the speed and expressive power of this mature probabilistic programming language.

My doctoral project was a theoretical investigation into dependent type theory. Dependent types form the basis for programming logics like Coq and Agda, which may be used to formalise logical reasoning and, in particular, give formal proofs about the correctness of computer programs. As it stands, only so-called pure dependently typed languages are well understood, in which crucial practical programming constructs like printing, recursion, mutable state, control operators, non-determinism and probabilistic choice are excluded. My DPhil contributed towards a better understanding of the possibilities of extending dependent types towards more realistic impure languages. This analysis was performed by looking at dependent types from the points of view of linear logic, game semantics and call-by-push-value. In particular, the thesis presented the first game theoretic analysis of dependently typed computation.

For my publications, see my Google Scholar profile.

Some slides of recent talks:

Past Research

Doctoral thesis giving a semantic analysis of how to combine dependent types with effectful computations, through the lens of linear logic, game semantics and call-by-push-value.

Master's thesis on topos-theoretic approaches to quantum kinematics, a survey article of the field, unifying some of the definitions and results and presenting some new ones.

Bachelor's thesis on principal bundles and gauge theory, a set of lecture notes that was intended to form an addition to the then existing literature by connecting the mathematical and physical parts of the story.