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 currently on the job market for a full-time industrial job of research and/or development starting Summer 2018. If you are interested, drop me a line!

I am a PhD candidate working at MIT CSAIL advised by Prof. Adam Chlipala.

I worked on a verified compiler from a C-like language called Cito to Bedrock. The Cito language supports expressions, usual control-flow constructs(if, while, etc.), dynamically allocated arrays, and function calls via function pointers. The callee functions can be either Cito functions or Bedrock functions written manually or compiled from other compilers. Hence our compiler supports verified compositional compilation. Cito functions can be recursive (self-recursive and/or mutual-recursive). Everything is written and proved in the Coq proof assistant.

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. 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. The Coq source code is open-sourced.

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, 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 both my Bachelor of Engineering (BE) and Master of Science (MS) degrees from the Department of Computer Science and Technology at Tsinghua University, Beijing, China, in the year 2010 and 2012 respectively. My MS reserach was in the field of computer vision advised by Chinese Academy of Sciences (CAS) Fellow Prof. Bo Zhang.


Spring 2016: TA for MIT 6.887 Formal Reasoning About Programs


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

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

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

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


Github page


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