I am a second year PhD student at the University of Michigan in Computer Science and Engineering working with Jean-Baptiste Jeannin and Max New.

My research interests are primarily in the logic and semantics of programming languages. In particular I am interested in the application of category theory and type theory to inform the design, implementation, and verification of programming languages.

More broadly, I am a huge proponent of intuitionistic mathematics demonstrated to a computer — such as in a proof assistant. The Curry-Howard Correspondence extends in two directions: just as we use mathematics to inform our analysis of computation, we should take a computational point-of-view to give an unambiguous and constructive accounting of mathematics.