I am a PhD student under the supervision of Marc Aiguier and Gilles Dowek, in the MICS laboratory at CentraleSupélec and in the Deducteam at Laboratoire Méthodes Formelles.
As a student, I was part of the research curriculum of CentraleSupélec, under the supervision of Valentin Blot and Gilles Dowek, at Laboratoire Méthodes Formelles. My work was focused on the λΠ-calculus modulo theory and the Lambdapi proof assistant. In particular, I implemented an encoding of set theory in Lambdapi. Working with Théo Winterhalter, I studied the replacement of rewrite rules by axioms inside the λΠ-calculus modulo theory.
Research interests
- Logical frameworks
- Type theory
- Rewrite rules
- Intuitionistic logic
Publications
- From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory
[PDF]
with Valentin Blot, Gilles Dowek and Théo Winterhalter
27th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2024) - Rewrite Rules in the λΠ-Calculus Modulo Theory
Master thesis, CentraleSupélec, 2023. - An Implementation of Set Theory with Pointed Graphs in Dedukti
[PDF]
with Valentin Blot and Gilles Dowek
17th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2022)
Talks
- 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, 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
- Modélisation logique & Langages et automates, CentraleSupélec, 2023-2024
Contact
Email: thomas (dot) traversie (at) centralesupelec (dot) fr