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.
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
-
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.
News
-
January 22, 2022
Presenting Tealeaves at CoqPL 2022 workshop. -
February 12, 2020
I will be visiting EPFL in Marchcancelled due to COVID-19
-
December 10, 2019
New website launched -
December 9, 2019
Finished with qualifying exams