I am currently pursuing a Ph.D. degree at the Formal Verification Group under the supervision of Dr. Mingshuai Chen. My research interest lies in programming language theory, static analysis and theorem proving. I am currently focusing on the compositional theory of programming languages, including their formal semantics and logic, with the help of type-theory-based proof assistants.