I’m a PhD student in MIT’s Programming Languages and Verification group (PLV). I’m currently in the exploratory phase of working on lattice-based crypto in the proof assistant Coq. I’m also continuing my longstanding work with fiat-crypto, another Coq project which generates verified code for ECC primitives. Both of these projects amount to using the proof assistant to guatantee that pieces of cryptography code actually implement their algorithmic specifications.

My general areas of interest include distributed systems and computer security, particularly in relation to verification. I’m also interested in how to effectively introduce people to programming, both generally and for specialized contexts like verification.