I’m a Researcher in the RiSE 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

F* is the main programming language used in the Everest expedition, a project that aims to build and deploy a verified, drop-in replacement of the HTTPS stack, a lynchpin of internet security. I co-lead Everest and the project includes researchers from MSR Redmond, MSR Cambridge, MSR India and INRIA Paris.



Project Everest – Verified Secure Implementations of the HTTPS Ecosystem

Established: May 31, 2016

Summary Project Everest aims to build and deploy a verified HTTPS stack. The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle,…

The F* Project

Established: March 25, 2011

F* is a verification-oriented dialect of ML. For more information, please visit https://fstar-lang.org or click on the logo below.










I have been in the past or am currently the co-chair of PLAS 2013 and PLPV 2012.

I am serving (or have served) on the program committees for ICFP 2017, Oakland 2017,  Oakland 2016, ML 2016POST 2016, CSF 2015,  POPL 2014, POST 2014, DTP 2013, ICFP 2013, PLACES 2013, TFP 2013, HOPE 2012TFP 2012, CSF 2012, PLACES 2012POST 2012, CSF 2011, PLAS 2011, FTfJP 2010; and on the external review committee for POPL 2012.

Some recent talks: 

Functional Geekery (podcast interview about F*) 2016

Dijkstra monads for free: A framework for deriving and extending F*’s effectful semantics; Invited talk at ITP 2016 (Interactive Theorem Proving)

The ICFP Contest 2013: Calibrating research on program synthesis; Contest chairs’ report at the International Conference on Functional Programming (ICFP), 2013

Certified correctness for higher order programs; Invited talk at VSTTE (Verified Software: Theories, Tools and Experiments) 2013

Taming JavaScript with F*; Keynote at HCSS (High Confidence Software and Systems) 2013

Some of my old (pre-2008) projects are available from University of Maryland’s programming languages research group.