I am a second-year Masters (M2) student studying the Parisian Master of Research in Computer Science (MPRI) at École Polytechnique. My research interests lie in logic, verified proofs, and proof assistants (such as Rocq and Agda).

In my Masters Year 1 internship, I worked towards formalising the guard checker of Rocq with Yannick Forster in the Cambium research team in Inria Paris. In my report, I documented the guard checker with examples and explanations. The full implementation is freely accessible online.

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 honors college of NUS.

News

• 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.
• 25 October 2024: My Masters 1 Project/Thesis received an Honourable Mention (“Mention de Félicitations”) from École Polytechnique!
• 15-21 September 2024: I attended the Proof and Computation Autumn School 2024, at Fischbachau, Germany.
• 14 September 2024: I will be presenting (remotely) at the Coq Workshop 2024 about my M1 internship project on the Guard Checker of Rocq. It is affiliated with ITP 2024 at Tbilisi, Georgia.
• 27 August 2024: I successfully defended my Masters 1 internship, in which I implemented the Guard Checker of Rocq in MetaRocq and documented its behaviour! Here are the code, report, and slides.

Talks

• Towards Formalizing the Guard Condition of Rocq, 24 September 2024
  Talk at Coq Workshop 2024.
  Joint work with Yannick Forster.
• Towards Formalizing the Guard Condition of Rocq, 3 June 2024
  Invited talk at Workshop on the guard condition of Coq, RECIPROG.
  Joint work with Yannick Forster.

Theses

• Towards Formalising the Guard Checker of Rocq
  Masters Year 1 Thesis, École Polytechnique, 2024.
  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.
  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

• 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.