Yee-Jian Tan
PhD student at DistriNet, KU Leuven. Implementing Type Theories into Proof Assistants.
I am a PhD student at DistriNet, KU Leuven, Belgium, working with Dominique Devriese and Andreas Nuyts on implementing Multimodal Type Theory in Agda. I am also continuing work from my M2 internship on adding computational rules for UIP in Cubical Agda. My research interests lie in logic, verified proofs, and proof assistants (such as Rocq and Agda).
Previously in 2025, I obtained the Parisian Master of Research in Computer Science (MPRI) at École Polytechnique. In my Masters Year 2 internship, I worked towards implementing computational UIP in Cubical Agda (report, code) with Dominique Devriese and Andreas Nuyts. In my Masters Year 1 internship, I worked towards formalising the guard checker of Rocq (report, code) with Yannick Forster in the Cambium research team in Inria Paris.
Previously, I obtained my Bachelor’s Degrees in Mathematics and Computer Science at the National University of Singapore. I wrote my thesis on the formalization of Rocq Modules in the MetaRocq project, co-supervised by Nicolas Tabareau, Martin Henz, and Yue Yang. I was also part of the University Scholars Programme, the honours college of NUS.
If you are interested in my research, looking for collaboration, or having any questions about getting into type theory research (MPRI, etc), please do not hesitate to get in touch with me!
News
- 6 May 2026: I will be giving a talk about the current Cubical-UIP implementation at the TYPES 2026 in Gothenburg, Sweden.
- 24 November 2025: I gave a talk about Cubical-UIP at the 41st Agda Implementor’s Meeting in Angers, France.
- 19 September 2025: I am starting my PhD on implementing Multimodal Type Theory, at DistriNet, KU Leuven, Belgium, supervised by Dominique Devriese and Andreas Nuyts.
- 2 September 2025: I successfully defended my Masters Year 2 (M2) Project/Thesis on “Towards Computational UIP in Cubical Agda”!
Talks
- Towards Computational UIP in Cubical Agda
Joint work with Andreas Nuyts, Dominique Devriese. - Towards Formalizing the Guard Condition of Rocq
Joint work with Yannick Forster. - A Stepper for a Functional JavaScript Sublanguage
Joint work with Martin Henz, Thomas Tan, Zachary Chua, Peter Jung, Xinyi Zhang, and Jingjing Zhao, 2021.
Talk at SPLASH-E 2021 (slides).
Theses
-
Towards Computational UIP in Cubical Agda
Masters Year 2 Thesis, IP Paris (École Polytechnique), 2025.
Supervised by Andreas Nuyts, Dominique Devriese.
Report, Slides, Code. -
Towards Formalising the Guard Checker of Rocq
Masters Year 1 Thesis, IP Paris (École Polytechnique), 2024.
Supervised by Yannick Forster.
Honourable Mention (“Mention de Félicitations”) by École Polytechnique on L3/M1 Theses.
Report, Slides, Code. -
Formalizing Rocq Modules in the MetaCoq Project
Bachelor’s Thesis, National University of Singapore, 2023.
Supervised by Nicolas Tabareau, Martin Henz, Yue Yang.
Report, Slides, Code.
Projects and Reports
- Formalizing Dependent Types in Agda (~equivalent to 1-month internship)
Supervised by Ambrus Kaposi.
Publications
- A Stepper for a Functional JavaScript
Sublanguage.
Joint work with Martin Henz, Thomas Tan, Zachary Chua, Peter Jung, Xinyi Zhang, and Jingjing Zhao, 2021.
Proceedings of the 2021 ACM SIGPLAN International Symposium on SPLASH-E, October 2021, pp. 71–81.
CV
-
2025: Masters in Computer Science Research (Master Parisien de Recherche en Informatique (MPRI)).
Institut Polytechnique de Paris (École Polytechnique).
Magna cum Laude. -
2023: B.Comp (Hons) Computer Science (Distinction), National University of Singapore.
Focus area: Algorithms and Theory -
2023: B.Sc (Hons) Mathematics with (Highest Distinction), National University of Singapore.
Focus areas: Logic, Abstract Algebra
Click here for a full CV.