I am a PhD student at DistriNet, KU Leuven, Belgium, working with Dominique Devriese and Andreas Nuyts on implementing Multimodal Type Theory in 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

• 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”!
• 13 June 2025: I gave a talk on the Guard Checker of Rocq (slides, recording) at TYPES 2025 in Glasgow, Scotland.
• 1 April 2025: I am starting my Masters Year 2 (M2) internship at KU Leuven with Andreas Nuyts and Dominique Devriese, working on implementing new type theory primitives in the Agda proof assistant.

Talks

• Towards Formalizing the Guard Condition of Rocq
  Joint work with Yannick Forster.
  • Talk at TYPES 2025 (slides), 13 June 2025.
  • Talk at Coq Workshop 2024 (slides), 24 September 2024.
  • Invited talk at the Workshop on the guard condition of Coq, RECIPROG (slides), 3 June 2024.
• 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.