I’m a Senior Principal Researcher in the RiSE (opens in new tab) group at MSR Redmond. My work covers various topics including type systems, program logics, functional programming, program verification and interactive theorem proving. I often think about how to use these techniques to build provably secure programs, including web applications, web browsers, crypto protocol implementations, and low-level systems code.
Many of my current projects connect somehow to F*, a programming language and verification tool for higher-order, effectful programs. You can learn more about F*, including trying an interactive tutorial, at https://fstar-lang.org (opens in new tab)
F* is the main programming language used in Project Everest (opens in new tab), an effort to build and deploy provably secure communication software that I co-lead.