Resume
I am a 1st year phd student in the Gallinette team
at Inria & Nantes University,
under the direction of Nicolas Tabareau, Yannick Forster,
and Matthieu Sozeau.
I am working on Proof Assistants, most particularly on generating recursors for
inductive types using MetaCoq, and towards formalising Coq’s guard condition.
On the side of my phd, I am pushing forward the project Coq Platform Docs aiming at documenting Coq and its Platform.
I am also working on some other projects linked to initial semantics :
- Leveraging the parametricity of initial semantics framework in the input monoidal category with Ambroise Lafont
- Reformulating and extending some notions of initial semantics to polymorphic languages with Benedikt Ahrens and Ambroise Lafont
Research Internship
As my 3rd at Ens Paris-Saclay, I am starting in October 2022, a 9 months research internship with Benedikt Ahrens. The project will be to extend the framework of initial semantics (in the tradition of monads-based models) with polymorphism.
For my second semester of first year of Master, I will do a 6 months research internship with Anders Mörtberg. The project will be to attempt to formalize cohomology rings, in univalent synthetic mathematics in Cubical Agda
For my last year of bachelor, I will do a 2 months research internship with Nicolas Tabareau. The project will be to reformulate the framework of univalent parametricity to fully size to CIC omega
Education
Attend Ens Paris-Saclay in theoretical computer science. Amounting to a master in research in theoretical computer science and a second general research master.
Attend preparatory classes to french national competitive exams to engineering and research schools. Orientation theoretical mathematics and theoretical physics with an option in theoretical computer science.