Termination of λΠ modulo rewriting using the size-change principle (work in progress). - Frédéric Blanqui; Guillaume Genestier (CoRR, 2018)

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. - Frédéric Blanqui; Guillaume Genestier; Olivier Hermant (FSCD, 2019)

Encoding Agda Programs Using Rewriting. - Guillaume Genestier (FSCD, 2020)

Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting. (Terminaison en présence de types dépendants et encodage par réécriture d'une théorie des types extensionelle avec polymorphisme d'univers). - Guillaume Genestier (2020)