I joined MSR RiSE in September 2016, working on the Everest project: verified implementations of TLS and derivatives, using and extending the F* higher-order, effectful, dependently typed programming language.
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. Previously, in 2012, I defended my PhD thesis at INRIA and Université Paris Diderot, directed by Dr. Xavier Leroy, on verified compilation for C++ objects. See my external website for more information on my pre-MSR research and publications.