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

• The preprint for my survey of meta-programming in proof assistants (with Yannick Forster) is up on HAL.
• I will start a PhD with Yannick Forster and François Pottier around September 2025, working on meta-programming in proof assistants (mainly Rocq).
  
• I started an internship with Théo Winterhalter in March 2025, working on autosubst.