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

I started my PHD in october 2025

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

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
- S1 exercise sessions of the rewriting course of the M1 MPR1 at ENS Paris Saclay
  TD1
  TD2
  homework
  TD3
  TD4
  TD5
  TD6
- S2 (to be confirmed) Logic Project of the L3 Computer Science of ENS Paris Saclay

my CV (in french)