My work focuses on the computational content of deductive systems, from the perspective of graphical deduction systems. Currently, I work on three-dimensional diagrams for multiplicative linear logic. The goal is to understand better the complexity of proof equivalence for non-commutative fragments of this logic. To do so, I formalize linear logic proofs as string diagrams with Globular. In the future, I would like to explore the complexity of rewriting in categories generated by other signatures, and implement rewriting strategies in Globular.
On the side, I work on open science projects, most of which can be found on my GitHub profile.
I started my DPhil in October 2016, under the supervision of Jamie Vicary.
Before that, I studied at École Normale Supérieure, in Paris. For my masters degree in mathematical logic and foundations of computer science, I took a research placement at the University of Ljubljana where I worked with Alex Simpson on algorithmic randomness and point-free topology.