About me

I'm a PhD student in the Functional Programming Lab in the University of Nottingham. In 2024, I graduated from the Cambridge Mathematical Tripos. The notes I took on all of my courses at Cambridge are publicly available here.

My research focuses on the semantics of borrowing, a language feature allowing a logical resource to be loaned out by its owner. Loaned variables can be used immutably in a variety of ways, but these loans may expire at some point in the program, allowing the original owner to reclaim unique ownership. This paradigm has been used extensively by languages like Rust and Austral. I'm researching what borrowing is and why it works, at an abstract level.

Since 2022, I've been working with Randall Holmes on formalising a proof of the consistency of Quine's 1937 set theory New Foundations. Our main goal has now been completed: we now have a formal verification that Holmes' proof is correct. I'm still working on refactoring the code and the paper to make it easier to read and understand, and you can find my code here.