Welcome

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.

Email

Github

LinkedIn

Recent Posts

• Intro to string diagrams for monads — December 12, 2021
  Visualing monad laws and the Kleisli category using string diagrams
• Yes, monads are container-like — November 13, 2021
  A common intuition is that monads are like "containers" of values. How do we make sense of this formally?
• Using Hakyll as a Lightweight CMS — March 21, 2020
  Building the UPenn PL Club website with Hakyll and elbow grease.

See all posts.