I'm building neural networks that generate provably correct code, and the software infrastructure for training them.

I work on three fronts:

1. New architectures: Understanding old, and designing new neural networks that consume and produce structured data
2. Mathematical Foundations: Formalising what it even means to generalise when your inputs are not numbers, but datatypes
3. Infrastructure: Building the stack required to train neural networks in dependently-typed languages: tensor processing, automatic differentiation and elaborator integration

In all of these, I use category theory, the mathematics of structure and composition, as a central glue. To read more about my research programme, check out this link. To find my academic work, click here.