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.
Verified Low-Level Programming Embedded in F* [ Link ] [ arXiv ]
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
The End of History? Using a Proof Assistant to Replace Language Design with Library Design [ Link ]
Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang and Katherine Ye
Everest: Towards a Verified, Drop-in Replacement of HTTPS [ Link ]
(Alphabetically) Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Cătălin Hriţcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué
Extracting from F* to C: a progress report [ Link ] [ PDF ]
Peng Wang, Karthikeyan Bhargavan, Jean-Karim Zinzindohoué, Abhishek Anand, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
The Facade Language [ PDF ]
MedLSVM And Its Application To Structural Object Detection Models [ PDF ]
Master Thesis, 2012
Traffic Sign Detection [ PDF ]
Bachelor Thesis, 2010
Spring 2016: TA for MIT 6.887 Formal Reasoning About Programs
Inspired by Adam Chlipala's Book Log, here is my Book Log listing the books I have read or am reading (nonexhaustive).