Current Research

My doctoral project is 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 contributes towards a better understanding of the possibilities of extending dependent types towards more realistic impure languages. This analysis has so far been performed by looking at dependent types from the points of view of linear logic, game semantics and call-by-push-value.

Recently, I have been working on probabilistic programming with Neil Dhir. Specifically, we are modelling lion behaviour using Bayesian non-parametrics.

Some of my musings:

Some slides of recent talks:

Past Research

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.