Bio

I am a first year Ph.D. student under Max New.

Broadly, my research interests span both pure (topos theory and categorical logic) and applied (verification of software and hardware, formal mathematics, implementation of theorem provers) aspects of type theory. I am a proponent of mathematically driven approaches to programming language and type theory research. My goal is to work on projects that enable the creation of the next generation of interactive theorem provers. This includes researching new core calculi, semantics for these core calculi, and implementation methods.