I joined MSR RiSE in September 2016, working with Dr. Nikhil Swamy on the F* higher-order, effectful, dependently typed programming language, and with Dr. Leonardo De Moura on the Lean proof assistant, as part of the Everest project: specification and verification of a reference HTTPS client/server implementation.
My research interests span programming languages and formal methods, especially formal verification, language semantics, verified compilation.
Prior to joining MSR, I worked with Prof. Zhong Shao at Yale University on the CertiKOS verified operating system: compositional verification of layered software systems and verified separate compilation using the Coq proof assistant and the CompCert verified compiler. Previously, in 2012, I defended my PhD thesis at INRIA and Université Paris Diderot, directed by Dr. Xavier Leroy, on mechanized formal semantics and verified compilation for C++ objects. See my external website for more information on my pre-MSR research and publications.