I am a PhD student in Computer Science at the University of Toronto, where I’m part of the ProSE group. I work under the guidance of Prof. Ningning Xie and Prof. Fan Long.
Previously, I was a research intern at UC Santa Barbara, supervised by Prof. Yu Feng. Before that, I completed my B.Eng. in Computer Science at Shanghai Jiao Tong University, collaborating with Prof. Qinxiang Cao on compiler correctness verification.
My research revolves around Programming Languages. I focus on practical concepts and techniques that help people build sound and efficient softwares in a principal way.
Topics I'm currently exploring include:
- Expressive type theory and systems (row polymorphism, linear types, etc.)
- Powerful language features (e.g. staging, effect) done in a type-safe way
See also: CV
News
- November 2025: New paper accepted to POPL'26.
- August 2025: New paper accepted to OOPSLA'25.
- July 2025: I'm attending AOSCC25 at the end of July.
- June 2025: I'm attending OPLSS25 at the end of June.
- June 2025: New paper accepted to SBC'25.
Publications
Extensible Data Types with Ad-Hoc Polymorphism
Matthew Toohey, Yanning Chen, Ara Jamalzadeh, Ningning Xie
POPL 2026
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Junrui Liu, Jiaxin Song, Yanning Chen, Hanzhi Liu, Hongbo Wen, Luke Pearson, Yanju Chen, Yu Feng
OOPSLA 2025
Tessel: An Optimizing Compiler for Efficient Zero-Knowledge Circuits
Junrui Liu, Jiaxin Song, Yanning Chen, Hanzhi Liu, Hongbo Wen, Yanju Chen, Yu Feng
SBC 2025
Research Projects
Verification-aided Source Code Optimization
In prep
advised by Prof. Qinxiang Cao at JHC@SJTU
TAing
- CSC2126: Topics in Programming Languages. Fall 2025
- CSC324: Principles of Programming Languages. Fall 2025
- CSC2125: Blockchain Technology and Engineering. Winter 2025
- CSC324: Principles of Programming Languages. Fall 2024
Services
Subreview: ICFP 2025
Materials
- Navigating Proof Search in Theorem Provers
Seminar, ProSE@UToronto [PDF] [Typst] - An Introduction to Logical Relations
Seminar, ProSE@UToronto [PDF] [Typst] - Rustbelt, a formalization of Rust type system
Seminar, ProSE@UToronto [PDF] [Typst] - Interaction Trees: A denotational semantics and its equational theorems
Paper sharing talk, PLSE Lab@UCSB [PDF] [KeyNote] - Reading notes on PL related topics
Blog, zh-CN [GitHub]
