I am a PhD student in the Computer and Information Science department at the University of Pennsylvania, where I am advised by Val Tannen and Steve Zdancewic. My interests lie in the so-called computational trilogy and the theoretical foundations of computer science, with an eye towards applications in computer-verified formal reasoning.

My current research investigates a category-theoretic definition of syntax with variable binding using a class of monads equipped with multiple kinds of additional structure. This work facilitates a more generic approach to reasoning about formal systems such as lambda calculi and programming languages. I have formalized much of this theory in the proof assistant Coq, and you can browse the corresponding Github repository or read the documentation.

Prior to UPenn, I studied theoretical computer science and mathematics at Oxford and Florida State University.

Recent Posts

See all posts.


  • Presenting Tealeaves at CoqPL 2022 workshop.

  • I will be visiting EPFL in March

    cancelled due to COVID-19

  • New website launched

  • Finished with qualifying exams