From Rewrite Rules to Axioms in the $ lambda varPi $-Calculus Modulo Theory. - Valentin Blot; Gilles Dowek; Thomas Traversié; Théo Winterhalter (FoSSaCS (2), 2024)

From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory. - Valentin Blot; Gilles Dowek; Thomas Traversié; Théo Winterhalter (CoRR, 2024)

Kuroda's Translation for Higher-Order Logic. - Thomas Traversié (CoRR, 2024)

Kuroda's Translation for the λπ-Calculus Modulo Theory and Dedukti. - Thomas Traversié (LFMTP@FSCD, 2024)

Proofs for Free in the λπ-Calculus Modulo Theory. - Thomas Traversié (LFMTP@FSCD, 2024)

Monad Translations for Higher-Order Logic. - Thomas Traversié (FSCD, 2025)

Formalizing Representation Theorems for a Logical Framework with Rewriting. - Thomas Traversié; Florian Rabe 001 (CoRR, 2025)