I'm a PhD student in programming languages working with Amal Ahmed and Steven Holtzen at Northeastern University. I'm interested in logic, semantics, and mechanized proof. Lately I've been thinking about connections between mutable state and probability theory, and trying to learn synthetic X for various X. Before starting my PhD, I built a verified-optimization-pass generator as part of the CertiCoq project. When I'm not thinking about research, I like learning math, playing bullet chess, violin, and ping pong.