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.
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.
thomas (dot) traversie (at) centralesupelec (dot) fr
Research interests
- Intuitionistic logic
- Logical frameworks
- Type theory
- Rewrite rules
Publications
Research papers
- 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
- 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
- Modélisation logique et systèmes formels, CentraleSupélec, 2024-2025
- Systèmes d'information et Programmation, CentraleSupélec, 2024-2025
- Algorithmique et complexité, CentraleSupélec, 2023-2024, 2024-2025
- Modélisation logique & Langages et automates, CentraleSupélec, 2023-2024
- Informatique théorique, CentraleSupélec, 2023-2024
Last update: .