Registered user since Sat 15 Aug 2020
I am a PhD Candiate at Cornell University in the area of Logic, Semantics, and Formal Methods, advised by Alexandra Silva. My research focuses on Outcome Logic, a reformulation of Hoare Logic with computational effects at its core. Outcome Logic consolidates the metatheory behind many variants of Hoare Logic, enabling extensible reasoning about different types of programs and tying together ideas developed over that last sixty years including the seminal work of Floyd and Hoare on program logics in the 1960s, extensions of Hoare Logic to nondeterministic and probabilistic programs, monadic effects, and the more recent emphasis on formal methods for incorrectness.
Before coming to Cornell, I worked as a software engineer for six years at Facebook. During that time, I was fortunate to have unique opportunities 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 invaluable experiences.
Contributions
2025
2024
SPLASH
- Author of Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects within the OOPSLA 2024-track
- Author of (Lightning Talk) Unified Analysis Techniques for Programs with Outcomes within the Doctoral Symposium-track
- Author of Unified Analysis Techniques for Programs with Outcomes within the Doctoral Symposium-track
- Author of Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers within the OOPSLA 2024-track
Formal Methods for Incorrectness
- Organizer in Organizing Committee within the Incorrectness-track
- Author of Welcome within the Incorrectness-track
- Session Chair of Opening (part of Incorrectness)
- Session Chair of Logics and Program Analysis (part of Incorrectness)
- Committee Member in Program Committee within the Incorrectness-track