Publications

• Towards Quantitative Inductive Families
  with Jeremy Yallop, accepted to TYPES 2024

• Defunctionalization with Dependent Types (extended version, code, demo)
  with Jeremy Yallop, accepted to PLDI 2023

Timeline

Jun 2024
Presentation at TYPES, for extended abstract Towards quantitative inductive families

Jun 2023
Presentation at PLDI, for conference paper Defunctionalization with dependent types

Jan 2023 - Now
PhD in Computer Science, University of Cambridge

Oct 2021 - Oct 2022
PartIII(MEng) in Computer Science, University of Cambridge (dissertation)

Oct 2021 - Oct 2022
BA in Computer Science, University of Cambridge

Other stuffs

I am into classical and rock music. You might see me in the audience in lots of recitals and concerts around Cambridge and London. I have a Roland FP-90 piano in my room that keeps me away from boredom and over-working, and I was the keyboardist in the Robinson college’s rock band before covid.

For your interest, I was born and grew up in GuangXi province, China. I moved to Beijing later on and this is where I’m based now (when I’m not at Cambridge).