Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, with Guillaume Genestier and Olivier Hermant, 23 pages, 2018.
Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewrite systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewrite systems. This improves previous results by Wahlstedt on one hand and the first author on the other hand to strong normalization and non-orthogonal rewrite systems. This new criterion has been implemented in the type-checker Dedukti.