Nikhil Swamy

About

I’m a Senior Principal 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 Project Everest, an effort to build and deploy provably secure communication software that I co-lead.