About Me

I am a second year Computer Science PhD student at Courant Institute of Mathematical Sciences, New York University, working with Prof. Joseph Tassarotti in the ACSys group.

My research interests lie broadly in programming languages and formal methods. I am currently working on completeness theorems about the Iris separation logic framework. Previously at NYU, I worked on effect handler-based extensible program logics in Iris.

In the summer and fall of 2023, I was an intern in Prof. Xinyu Wang’s group at the University of Michigan, and worked on SMT-based automated bounded equivalence verification for SQL queries as a follow-up of the VeriEQL project.

I received my B.E. degree with honors from the University of Science and Technology of China in 2024. During my undergraduate study, I worked with Prof. Yu Zhang on foreign function interfaces of Go. My thesis is about Coq formalization of SQL query optimization rules, which is co-supervised by Prof. Yu Zhang and Prof. Xinyu Wang.