Since November 2026, I am a postdoctoral researcher in the Gallinette Inria team, at Laboratoire des Sciences du Numérique de Nantes, working with Assia Mahboubi and Nicolas Tabareau.
From 2023 to 2026, I was a PhD student under the supervision of Marc Aiguier, Gilles Dowek and Olivier Hermant, in the Arcade team at MICS laboratory and in the Deducteam at Laboratoire Méthodes Formelles. I worked on translations of proofs between logics and on the exchange of proofs within the Dedukti logical framework.
From 2020 to 2023, as part of my engineering studies at CentraleSupélec, I followed its research curriculum, working under the supervision of Valentin Blot and Gilles Dowek, in the Deducteam at Laboratoire Méthodes Formelles.
Research interests
- Proof theory
- Type theory
- Logical frameworks
- Proof translations
Publications
In journals
- Kuroda's Translation for Higher-Order Logic
To appear in the Journal of Symbolic Logic (JSL), 2026
[pdf]
In international conferences
- Investigations on Higher-Order Infinitary Logic
with Olivier Hermant and Marc Aiguier
11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)
[pdf] - Monad Translations for Higher-Order Logic
10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)
[pdf] - From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory
with Valentin Blot, Gilles Dowek and Théo Winterhalter
27th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2024)
[pdf] [appendices]
In international peer-reviewed workshops with proceedings
- Proofs for Free in λΠ-Calculus Modulo Theory
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2024)
[pdf] [implementation] - Kuroda's Translation for the λΠ-Calculus Modulo Theory and Dedukti
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2024)
[pdf] [implementation]
In international peer-reviewed workshops without proceedings
- Connecting Higher-Order Logics using Kolmogorov's Translation à la Dowek-Werner (long abstract)
Tribute to Gilles Dowek (TGD), 2026
[pdf] - An Implementation of Set Theory with Pointed Graphs in Dedukti
with Valentin Blot and Gilles Dowek
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2022)
[pdf] [implementation]
Manuscripts
- Formalizing Representation Theorems for a Logical Framework with Rewriting
with Florian Rabe
Under review, 2025
[pdf] [implementation]
Theses
- Translations of Proofs between Higher-Order Logics and between Theories with Rewriting
PhD thesis, Université Paris-Saclay, 2026. - Rewrite Rules in the λΠ-Calculus Modulo Theory
Master thesis, CentraleSupélec, 2023.
PhD Thesis
On September 24, 2026, I defended my PhD thesis, titled
This work was supervised by:
- Marc Aiguier, CentraleSupélec, Université Paris-Saclay
- Gilles Dowek, Inria and Université Paris-Saclay
- Olivier Hermant, Mines Paris, Université PSL
- Xavier Urbain, Lyon 1 Université, President
- Assia Mahboubi, Inria and Nantes Université, Reviewer
- Frank Pfenning, Carnegie Mellon University, Reviewer
- Delia Kesner, Université Paris Cité, Examiner
- Sara Negri, University of Genoa, Examiner
- Elaine Pimentel, University College London, Examiner
Talks
- Investigations on Higher-Order Infinitary Logic, FSCD 2026, July 2026 [slides]
- Connecting Higher-Order Logics using Kolmogorov's Translation à la Dowek-Werner, Tribute to Gilles Dowek Workshop, July 2026 [slides]
- Morphisms between Dedukti Theories, ICSPA meeting, January 2026 [slides]
- Monad Translations for Higher-Order Logic, Journées GT Scalp, October 2025 [slides]
- Monad Translations for Higher-Order Logic, FSCD 2025, July 2025 [slides]
- Translation Templates between Dedukti Theories, KWARC Seminar, February 2025 [slides]
- Generic Translations between Dedukti Theories, WG1+2+4 meeting, September 2024 [slides]
- Proofs for Free in the λΠ-Calculus Modulo Theory, LFMTP 2024, July 2024 [slides]
- Kuroda's Translation for the λΠ-Calculus Modulo Theory and Dedukti, LFMTP 2024, July 2024 [slides]
- Kuroda's Translation for Higher-Order Logic, Logimics Meeting, June 2024 [slides]
- Kuroda's Translation for Higher-Order Logic, LMF Séminaire au vert, June 2024 [slides]
- Replacing Rewrite Rules by Equational Axioms in the λΠ-Calculus Modulo Theory, LMF PhD Seminar, May 2024 [slides]
- From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory, FoSSaCS 2024, April 2024 [slides]
- Règles de Réécriture dans le λΠ-Calcul Modulo Théorie, Master thesis Defense, December 2023 [slides]
- An Implementation of Set Theory with Pointed Graphs in Dedukti, LFMTP 2022, August 2022 [slides]
Teaching
- Algorithmique et complexité, CentraleSupélec, 2023-2024, 2024-2025
- Systèmes d'information et Programmation, CentraleSupélec, 2024-2025
- Coding Weeks, CentraleSupélec, 2025-2026
- Modélisation logique et systèmes formels, CentraleSupélec, 2024-2025, 2025-2026
- Modélisation logique, CentraleSupélec, 2023-2024, 2024-2025
- Langages et automates, CentraleSupélec, 2023-2024
- Informatique théorique, CentraleSupélec, 2023-2024, 2024-2025
Last update: .