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.
In general, I am interested in the intersection of theory and practice in the field of programming language, things like normalization by evaluation, contextual type tyeory, bidirectional type systems, etc.
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
- Towards Quantitative Inductive Families
with Jeremy Yallop, accepted to TYPES 2024
Talks
- 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.
Contact
Email: yh419 (at) cam (dot) ac (dot) uk