I am a PhD student under the supervision of Prof. Jamie Vicary at the Computer Laboratory of the University of Cambridge. Within the department, I work as a member of the Cambridge Logical Structures Hub (CLASH.)
My research interests are focused around internal languages of higher structures, such as higher dimensional categories. These normally take the form of dependent type theories, such as Homotopy Type Theory (HoTT) for groupoids, but I am also interested in diagrammatic calculi.
A good example of a project I am proud to have worked on is homotopy.io. It is a proof assistant which allows one to do constructions in synthetic homotopy theory entirely through a graphical calculus for finitely-presented semistrict globular n-categories. If this does not make much sense to you, try out this tutorial I wrote for the tool.
I was not always a Computer Scientist. My academic background prior to PhD life was in pure Mathematics: I did a B.Sc. in Mathematics at King’s College London, to then join Part III of the Mathematical Tripos at the University of Cambridge. I maintain an active interest in foundations of Mathematics.
Preprint with Jamie Vicary, 2023.
We now have a wide range of proof assistants available for compositional reasoning in monoidal or higher categories which are free on some generating signature. However, none of these allow us to represent categorical operations such as products, equalizers, and similar logical techniques. Here we show how the foundational mathematical formalism of one such proof assistant can be generalized, replacing the conventional notion of string diagram as a geometrical entity living inside an n-cube with a posetal variant that allows exotic branching structure. We show that these generalized diagrams have richer behaviour with respect to categorical limits, and give an algorithm for computing limits in this setting, with a view towards future application in proof assistants.
Zeta-regularized Lattice Field Theory with Lorentzian background metrics
Lattice field theory is a very powerful tool to study Feynman’s path integral non-perturbatively. However, it usually requires Euclidean background metrics to be well-defined. On the other hand, a recently developed regularization scheme based on Fourier integral operator zeta-functions can treat Feynman’s path integral non-pertubatively in Lorentzian background metrics. In this article, we formally zeta-regularize lattice theories with Lorentzian backgrounds and identify conditions for the Fourier integral operator zeta-function regularization to be applicable. Furthermore, we show that the classical limit of the zeta-regularized theory is independent of the regularization. Finally, we consider the harmonic oscillator as an explicit example. We discuss multiple options for the regularization and analytically show that they all reproduce the correct ground state energy on the lattice and in the continuum limit. Additionally, we solve the harmonic oscillator on the lattice in Minkowski background numerically.
The homotopy.io proof assistant allows the construction of composite morphisms in a finitely-generated semistrict n-category, via a point-and-click user interface. Composites are rendered as 2d and 3d geometries, and can be visualised in 4d as movies of 3d geometries. Beyond its features as a visual proof assistant, homotopy.io can also be used as an effective tool to typeset string diagrams: any 2d diagram constructed in the proof assistant can be exported with ease into LaTeX/TikZ and SVG, with experimental support for manim. The proof assistant is implemented in the Rust programming language, and compiled to WebAssembly to run in the web browser.
I have given the following scientific talks:
- Posetal diagrams, ACT conference, Maryland (remote), August 3rd 2023,
- Posetal diagrams, YAMCATS seminar, Leeds, June 19th 2023,
- Posetal diagrams, POODLE seminar, Oxford, June 8th 2023,
- On some impossible properties of the affine line object, Part III seminar, Cambridge, April 3rd 2022.