I am a PhD student in computer science at the Laboratoire Méthodes formelles (LMF), on the subject of translating Isabelle proofs to Rocq (or Lean), supervised by Frédéric Blanqui.

News

Aligning HOL-Light and Rocq libraries formally, by me and Frédéric Blanqui, has been accepted at LPAR-26, where I will present our work

Presentations

I presented work from my 2025 internship online at the Rocqshop 2025
Presentation subject: “Automating alignments of HOL Light inductive types and recursive functions in Rocq”
Here are the slides and the recording.

2018-2021 Licence Parcours Spécial Mathématiques (Université Paul Sabatier, Toulouse)
Special Course Bachelor’s in Mathematics
2021-2023 Master Logique Mathématiques et Fondements de l’Informatique (LMFI) (Université Paris Cité, Paris)
Master’s in Mathematical Logic and Foundations of Computer Science
2023-2024 Préparation à l’Agrégation externe de Mathématiques (Université Paris Cité, Paris)
Preperation to the mathematics Agrégation, french national exam for secondary school teachers

This year (2026-2027) I am teaching the following:

exercises sessions of the proof theory course of the M1 MPRI at ENS Paris Saclay
the logic project of the L3 Computer Science of ENS Paris Saclay with (maybe) Raphaël Berthon
exercise sessions of the logic course of the L3 @ ENS

Here is what I taught on previous years:

2024-2025 Spent three months as an intern mathematics teacher at the Lycée de Villaroy in Guyancourt at the start of the scholar year
(classes for 2de GT and Tle STMG)
2025-2026
- exercise sessions of the rewriting course of the M1 MPR1
- the logic project (see this year’s course)

my CV (in french)