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 will be presenting work from my 2025 internship online at the
Rocqshop
2025
Presentation subject: “Automating alignments of HOL Light inductive
types and recursive functions in Rocq”
Education
2018-2021 Licence Parcours Spécial Mathématiques (Université Paul Sabatier, Toulouse)
Special Course Bachelor’s in Mathematics2021-2023 Master Logique Mathématiques et Fondements de l’Informatique (LMFI) (Université Paris Cité, Paris)
Master’s in Mathematical Logic and Foundations of Computer Science2023-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
Teaching
- 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 (with solutions)
TD2
homework (due 10/08) - S2 (to be confirmed) Logic Project of the L3 Computer Science of ENS Paris Saclay
- S1 exercise sessions of the rewriting
course of the M1 MPR1 at ENS Paris Saclay
Curriculum Vitae
my CV (in french)