I’m in my first year of PhD (adviser Derek Dreyer) in MPI-SWS, making investigations on proof-assistant-based formal verification of programs, in particular using Coq and Iris. I received my bachelor and master (adviser Fei He) both in Tsinghua University, where my research focus was on program synthesis and software merging. I enjoy cocktails, an art of mixing various components in a balanced and innovative way, just like inventing exciting new features for a programming language.
NOTE: this page is a more “casual” introduction of me and includes outcomes since undergraduate. It is under construction and some contents will be extended.
Interested Topics
- Type systems
- Formal semantics
- Proof assistants
- Program synthesis
- Probabilistic programming
- Repository mining & merge
- Compiler construction
Education
- Bachelor in Computer Science & Technology, Tsinghua University, 2017
- Master of Software Engineering, Tsinghua University, 2020
Teaching Assistant
- 30240382 Principles of Compilation, 2017 Fall
- 30240243 Operating Systems, 2018 Spring
- 30240382 Principles of Compilation, 2018 Fall
- 34100352 Functional Programming, 2019 Spring
- 44100484 Modeling and Verification of Software Systems I, 2019 Spring
- 30240382 Principles of Compilation, 2019 Fall
- 44100603 Software Analysis and Verification, 2020 Spring
All the above were at Tsinghua University.
Publications
- Fengmin Zhu, Fei He. Conflict Resolution for Structured Merge via Version Space Algebra. OOPSLA'18. DOI: https://doi.org/10.1145/3276536. Project website
- Fengmin Zhu, Fei He, Qianshan Yu. Enhancing Precision of Structured Merge by Proper Tree Matching. ICSE'19 Poster.
Selected Projects
- Decaf project: A simple education-purpose programming language for compiler courses
- LL1-Parser-Gen: An LL(1) parser generator in principle. (Used in the compilation course)
- Mastery: A more reasonable and neat three-way structured merge tool (now just for Java).
- ThuThesis-Starter: A starter template for new users of ThuThesis.
- Sudoku-BMC: A sudoku solver based upon NuSMV bounded model checker. (course project)
- LustreAST: A small tool to translate between the Lustre language and its AST representation. (course project)
- mydb: A simple one-user single-thread database. (course project)
Projects in MPI-SWS that I will work on and possibly contribute to in future:
Selected Talks
- TikZ 画“图”指南 (Tunight)
- Code is Cheap, Show Me the Proof (Tunight)
- Maybe, it’s a Monad! (Tunight)
- Future of Software Development? Program Synthesis and its Application (Course talk) [Slide]
- From OO, to OO: Subtyping as a Cross-cutting Language Feature [Slide]
Most of them were given in Chinese. Tunight is a traditional event held by TUNA.
Selected Cocktails
Negroni is one of my favorite cocktail and I tried plenty of variants (even one with Jägermeister). I have a telegram channel on cocktail making, though some of the comments are in Chinese.
Contact
Email: paulzhu at mpi-sws dot org