Peng (Perry) Wang 王鹏
me CSAIL, The Stata Center
77 Massachusetts Ave, 32-G822
Cambridge, MA 02139
Phone: 617-803-2025
Email: wangpeng at csail dot mit dot edu

I'm now on the job market for a full-time industrial research and/or development job starting Summer 2018. If you are interested, drop me a line!
I'm especially interested in infrastructure support for large-scale data analytics and machine learning (read the buzzword "machine learning" here as "SGD-based regressions";-)

I am a PhD candidate at MIT CSAIL advised by Prof. Adam Chlipala. My research fields are 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.


Publications

TiML: A Functional Language for Practical Complexity Analysis with Invariants (accepted) [ PDF ] [ GitHub ] [ Source Code ] [Web Interface]
Peng Wang, Di Wang, Adam Chlipala
OOPSLA 2017

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
ICFP 2017

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
SNAPL 2017

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é
SNAPL 2017

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
ML 2016

The Facade Language [ PDF ]
Peng Wang
Technical Report

Compiler Verification Meets Cross-Language Linking via Data Abstraction [ Link ] [ PDF ] [ Slides ]
Peng Wang, Santiago Cuellar, Adam Chlipala
OOPSLA 2014

MedLSVM And Its Application To Structural Object Detection Models [ PDF ]
Peng Wang
Master Thesis, 2012

A Real World Detection System: Combining Color, Shape and Appearance to Enable Real-time Road Sign Detection [ Link ] [ PDF ]
Peng Wang, Jianmin Li, Bo Zhang
VISAPP 2012

Traffic Sign Detection [ PDF ]
Peng Wang
Bachelor Thesis, 2010


Teaching

Spring 2016: TA for MIT 6.887 Formal Reasoning About Programs


Resume/CV

Github page

LinkedIn page

Other

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