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.)

See also: Resume

On-going Projects

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

For details and past projects, see works.

Materials

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