WELCOME!

I am a PhD student in Computer Science at Robinson College, University of Cambridge.

I work on type-preserving transformation and compilation for dependent type theory – preserving the rich and expressive type specifications of programs down to the assembly level.

I also care about creating efficient and practical implementations of dependently typed programming languages, such as normalization by evaluation and quantitative type theory.

Inquiries about Part II / Part III individual projects are welcome, and you can find my project suggestions on the teaching page.

Publications

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

Extended abstracts

• A Fully Dependent Assembly Language
  with Jeremy Yallop, submitted to TYPES 2025

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

Talks

• Substitution, Normalization, and Formalization, Apr 2025, at S-REPLS16. slides
• Substitution, Normalization, and Formalization, Dec 2024, at department’s Lunchtime Sandwich Seminar.
• Towards Quantitative Inductive Families, June 2024, at TYPES.
• Type-preserving Compilation For Dependent Types, Apr 2024, at Robinson College SCR/MCR Research seminar.
• Defunctionalization with Dependent Types, June 2023, at PLDI.

Service

• Artifact evaluation committee, PLDI 2025

Contact

Email: yh419 (at) cam (dot) ac (dot) uk