1600 Amphitheatre Parkway Mountain View, CA 94043 Email: wangp dot thu at gmail dot com

I am a Software Engineer on the TensorFlow team at Google Brain.

I got my PhD in Computer Science from MIT CSAIL advised by Prof. Adam Chlipala by defending this. My research fields were software formal verification and programming-language design.

I worked on a verified compiler from a C-like language named Cito to an assembly language named Bedrock. The compiler supports verified compositional compilation in the sense that each source module can be compiled separately and the target modules along with the proofs of the correctness their compilation can be linked together. Everything is written and proved in the Coq proof assistant. It is open-sourced here on Github (under directories Bedrock/Platform/Cito and Bedrock/Platform/Facade).

Currently I'm designing and implementing a new language called TiML (Timed ML) which is an ML-like (surprise!) language with a type system containing time complexity annotations. Type will prevent you from calling an O(n^2) function when what you want is an O(n*log(n)) one. It supports refinement annotations (as in refinement types) and big-O complexity inference which allow programmers to verify the time-complexities of complex data structures and algorithms (e.g. reb-black trees and Dijkstra's shortest-path algorithm). You can try it out on its Web interface.

In Summer 2014 I interned at Microsoft Research Cambridge mentored by Georges Gonthier on formalizing matrix differentiation with SSReflect of the Math Component Library. I also wrote a tool that generates LaTeX code from Coq code so that the equational proofs in machine-learning papers can be generated from rigorous proofs in Coq. The Coq source code of the matrix-differentiation library is open-sourced here.

In Summer 2016 I interned at Microsoft Research Redmond mentored by Jonathan Protzenko and Nikhil Swamy on the F* language and Project Everest, where I proved the translation from Low* (a first-order fragment of F*) directly to C* (a fragment of C) for both functional correctness and side-channel-attack resilence. The work led to our ICFP 2017 paper Verified Low-Level Programming Embedded in F*.

I got my Bachelor of Engineering (BE) and Master of Science (MS) degrees both from the Department of Computer Science and Technology of Tsinghua University, Beijing, China, in year 2010 and 2012 respectively. My MS research was in Computer Vision, advised by Chinese Academy of Sciences (CAS) Fellow Prof. Bo Zhang.

Spring 2016: TA for MIT 6.887 Formal Reasoning About Programs

Other

Inspired by Adam Chlipala's Book Log, here is my Book Log listing the books I have read or am reading (nonexhaustive).