I am a final year PhD Candidate 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 the 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 programs that branch into different outcomes, which provide a unifying perspective for reasoning about a wide variety of effects including nondeterminism, nontermination, randomization, concurrency, and exceptions. Through my research, I have developed Outcome Logic, which has applications including:
Correctness & Incorrectness. Outcome Logic bridges reasoning about the absence of errors (correctness) and the presence of bugs (incorrectness). Whereas prior techniques were specialized to one modality, Outcome Logic enables new forms of static analysis by incorporating elements from both styles.
Probabilistic Concurrency. By composing multiple types of effects, I have developed an expressive foundation for the analysis of randomized distributed algorithms, which goes beyond prior approaches in its ability to reason about probabilistic behavior. Applications include verification of security, privacy, and blockchain algorithms.