CSAIL, The Stata Center
77 Massachusetts Ave, 32-G822
Cambridge, MA 02139
Email: wangpeng at csail dot mit dot edu
I am a PhD candidate working at MIT CSAIL advised by Prof. Adam Chlipala. I'm currently working 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.
I got my Bachelor of Engineering (BE) and Master of Science (MS) degrees both 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.
Compiler Verification Meets Cross-Language Linking via Data Abstraction (accepted)
Peng Wang, Santiago Cuellar, Adam Chlipala.
Inspired by Adam Chlipala's Book Log, here are the books I have read or am reading (unexhaustive).