B.Eng in Computer Science @ Shanghai Jiao Tong University (2019 - present)
Generally interested in PL concepts and techniques that helps people build correct and efficient software, especially in a correct-by-construction way. I mainly worked on deductive verification and compiler correctness, and also did some work on DSL design and synthesis.
And now, I'm interested in:
- Composable and expressive semantics (e.g. Interaction Trees)
- Interesting language features like staging and effect systems
- Beautiful and practical type theory and systems (e.g. row polymorphism, gradual typing, session types, etc.)
- Stuff that might rescue us from tedious proof engineering (e.g. proof synthesis and better HCI)
I'm actively applying for PhD programs in PL.
See also: Resume
On-going Projects
- Optimizing Compiler for ZK Circuits
advised by Prof. Yu Feng at CS@UCSB
- Verification-aided Source Code Optimization
advised by Prof. Qinxiang Cao at JHC@SJTU
For details, see works.
Materials
- Interaction Trees: A denotational semantics and its equational theorems
Paper sharing talk, PLSE Lab@UCSB [KeyNote] [PDF]
Designed by myself [1].
Last updated on 2023/12/8.