I am a PhD Candiate at Cornell University in the area of Programming Languages and Formal Methods, advised by Alexandra Silva. My research focuses on Outcome Logic, a logical framework for reasoning about programs that branch into many different traces due to nondeterminism, probabilistic choice, or other related computational effects. One goal of this work was to unify formal methods for correctness and incorrectness, whose metatheory had diverged into the semantically incompatible Hoare Logic and Incorrectness Logic.
My current research involves extending Outcome Logic with the ability to mix multiple kinds of effects. I am particularly interested in the combination of randomization and concurrency, with the ultimate goal of developing expressive techniques for reasoning about randomized distributed systems where probabilistic computation is often used in synchronization and cryptographic protocols. My research is supported in part by an Amazon Research Award, and I was recently recognized with the 2024 ACM SIGPLAN John Vlissides Award for applied software research.
Before coming to Cornell, I was a staff software engineer in the Facebook Programming Languages and Runtimes team, where I was fortunate to work on unique projects including using dependently typed Haskell in production, formally verifying concurrent algorithms for an OS microkernel, and experimenting with an information flow control type system for the Hack language. I strive to ground my research in these experiences.