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.
Service: I have been in the past or am currently the co-chair of PLAS 2013 and PLPV 2012; on the program committees for POPL 2014, POST 2014, DTP 2013, ICFP 2013, PLACES 2013, TFP 2013, HOPE 2012, TFP 2012, CSF 2012, PLACES 2012, POST 2012, CSF 2011, PLAS 2011, FTfJP 2010; and on the external review committee for POPL 2012. I also currently serve as the chair of of PL(X), the RiSE working group on programming languages.
Some recent talks:
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
Some of my old (pre-2008) projects are available from University of Maryland's programming languages research group.