Home
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
News
I will give at talk at the workshop Homotopy Type Theory and Computing - Classical and Quantum entitled “Computing Cohomology Rings in Cubical Agda” about our associated CPP paper.
I will be starting my master 2 research internship in march 2024, under the supervision of Nicolas Tabareau. We will investigate the generation of induction principles for nested inductive types in Coq.
I am happy to share our new preprint An Introduction to Different Approaches to Initial Semantics with Benedikt Ahrens, that aims at getting closer different approaches to initial semantics.
Our paper Computing Cohomology Rings in Cubical Agda with Axel Ljungström and Anders Mörtberg, was accepted at CPP 2023 and awarded Distinguished Paper.
In the paper, we explain how to formalize Cohomology Rings in synthetic mathematics. With a special focus on data structures and how they influence formalization, most noticeably the direct sum and (multivariate) polynomials.