About me

Hi! I am Hanzhi Liu (刘涵之, in Chinese). I am a junior student of EECS at Shanghai Jiao Tong University. I am advised by Professor Qinxiang Cao and work on compiler correctness and metaprogramming theory in Coq proof assistant.

Research Interests

I am interested in technologies that allow programs to be useful and bugless. In particular, I am committed to giving programs the ability to be proven correct end-to-end, so that they can be trusted formally. Currently, my research interests include Formal Verification , Programming Language and Blockchain.


  • [Sepetember 7, 2021] One participating paper about economics was submitted to Applied Economics.
  • [February 28, 2020] One first-author paper about COVID-19 modeling got accepted for Journal of Shanghai Jiao Tong University (Science).