I am 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. My PhD work focuses on the translation of proofs between logics and on the exchange of proofs within logical frameworks.
Before that, I was part of the research curriculum of CentraleSupélec, under the supervision of Valentin Blot and Gilles Dowek, at Laboratoire Méthodes Formelles. I implemented an encoding of set theory in the Lambdapi proof assistant. Working with Théo Winterhalter, I studied the replacement of rewrite rules by axioms inside the λΠ-calculus modulo theory.
Research interests
- Proof theory
- Type theory
- Logical frameworks
- Proof translations
Publications
Research papers
- Investigations on Higher-Order Infinitary Logic
with Olivier Hermant and Marc Aiguier
Submitted, 2026
- Formalizing Representation Theorems for a Logical Framework with Rewriting
with Florian Rabe
Submitted, 2025
[pdf] [implementation] - Monad Translations for Higher-Order Logic
10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)
[pdf] - 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] - Kuroda's Translation for Higher-Order Logic
Submitted, 2024
[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] - 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]
Theses
- Rewrite Rules in the λΠ-Calculus Modulo Theory
Master thesis, CentraleSupélec, 2023.
Talks
- 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 & Langages et automates, CentraleSupélec, 2023-2024
- Informatique théorique, CentraleSupélec, 2023-2024, 2024-2025
Last update: .