I am a PhD student in Computer Science at the University of Toronto. As a member of ProSE, I'm supervised by Prof. Ningning Xie and Prof.Fan Long.

Previously, I worked as a Research Assistant at UC Santa Barbara under the supervision of Prof. Yu Feng. I received my B.Eng. degree in Computer Science from Shanghai Jiao Tong University, where I worked with Prof. Qinxiang Cao on compiler correctness and formal verification.

I'm generally interested in Programming Languages concepts and techniques that helps people build sound and efficient softwares, especially in a correct-by-construction way.

To be specific, I'm currently exploring topics like:

• Interesting language features like staging and effect systems
• Beautiful and practical type theory and systems (e.g. row polymorphism, gradual typing, session types, etc.)

See also: Resume

Research Projects

Optimizing Compiler for ZK Circuits
In prep advised by Prof. Yu Feng at CS@UCSB

Verification-aided Source Code Optimization
In prep advised by Prof. Qinxiang Cao at JHC@SJTU

TAing

• CSC324: Principles of Programming Languages. Fall 2024

Materials

1. Rustbelt, a formalization of Rust type system
   Paper sharing talk, ProSE@UToronto [HTML] [PDF] [Markdown (Zipped)]

2. Interaction Trees: A denotational semantics and its equational theorems
   Paper sharing talk, PLSE Lab@UCSB [KeyNote] [PDF]

3. Reading notes on PL related topics
   Blog, zh-CN [GitHub]