I am a PhD Candiate at Cornell University in the area of Programming Languages and Formal Methods, advised by Alexandra Silva. 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 and formally verifying concurrent algorithms for an OS microkernel. My current research is supported in part by NSF (awards #2504142 and #2504143) and I was recently recognized with the 2024 ACM SIGPLAN John Vlissides Award for applied software research.
My research focuses on logical foundations for reasoning about randomized concurrent programs. For decades, randomization has been used to improve the performance and capabilities of distributed systems. For example, the Dining Philosophers–a distributed synchronization problem–has no fully distributed deterministic solution, but it has a simple randomized one. Establishing correctness for these types of programs is notoriously difficult because random sampling interacts in complex ways with concurrent scheduling. Through my research, I have made significant progress towards developing semantic models and formal methods for probabilistic concurrent programs.
My work builds on Outcome Logic, a logical framework that I previously developed 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.