About me

I am a 4-th year computer science student at ENS Paris, currently doing an internship at Inria Saclay in Deducteam. I’m interested in pushing the automation aspect of proof assistants such as Rocq, Agda, and Lean.

News

• I will be attending the SPLV summer school in July.
• I will start a PhD with Yannick Forster and François Pottier around September 2025, working on meta-programming in proof assistants (mainly Rocq).
  
• The preprint for my survey of meta-programming in proof assistants (with Yannick Forster) is up on HAL.