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