About me

I am a 4-th year computer science student at ENS Paris, currently doing an internship at Inria in the Cambium team. I’m interested in pushing the automation aspect of proof assistants such as Coq or Lean.

Previously I worked on compiling functional languages to GPUs with Mary Sheeran in Gothenburg.

News

• I started an internship with Yannick Forster in September 2024, working on metaprogramming in proof assistants based on dependent type theory.
  
• From March to August 2024 I did my Master’s internship with Benjamin Werner. We worked on Actema (try it !), a graphical user interface for Coq based on a drag-and-drop formalism. Take a look at this paper for more details on Actema.