Since high school studied how text could be transformed into programs, proofs or anything that makes sense. Trying to make the world self-compatible.

I am currently doing my PhD thesis with Cyril Cohen in ENS de Lyon. My work subject is Trocq, a Rocq library doing proof transfer. You can find most of my notes and presentation I made about this on my Inria gitlab.

Curriculum

Schools

2018-2021: High-school preparatory classes (CPGE)

Lycée Lafayette & Lycée Blaise Pascal Preparatory classes for the ENS competitive exam, extended to three years

2021-2025: ENS diploma curriculum

ENS de Lyon Licence degree in 2022, first year of master’s degree in 2023. Register as “external studies” for the second year of the Master’s degree. Fourth year of internships.

2023-2024: MPRI (Master Parisien de la Recherche en Informatique)

Université Paris Cité Second year of master degree outside of the ENS because of a course selection that fit my interests a lot more.

Internships

Summer 2022: Program Equivalences in (Featherweight) Java

8 week internship with Daniele Varacca & Clément Aubert in LACL, Créteil, France I did create an interesting notion of context and equivalence in this minimal object-oriented language.

Summer 2023: Logic as a Second-Order Generalized Algebraic Theory

3 month internship with Kaposi Ambrus & Thorsten Altenkirsch at ELTE, Budapest, Hungary I did implement a formalization of Propositional and First order Logic in Agda, based upon a SOGAT definition of those logics.

Summer 2024: Categorical semantics of the reduction of GATs to two-sorted GATs

4.5 month internship with Ambroise Lafont at LIX, Palaiseau, France I did prove a known GAT tranformation to be correct and to preserve some properties. This work lead to a publication in 2026 that you can find here: https://arxiv.org/abs/2601.19426

5 month internship with Kenji Maillard at LMU, München, Deutschland I studied Hyperdoctrines and implemented them in the Proof Assistant Lean, along with an extension to any modal logic, taking guarded logic as an example.

Spring 2025: Getting the hang of Trocq

3.5 month internship with Cyril Cohen at LIP, Lyon, France Applications and extensions of Trocq for formalized mathematics in proof assistants based on CIC