Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, with Guillaume Genestier, 18 pages, 2018, submitted to LPAR-22.
This paper is about the termination of typed higher-order rewrite systems. Dependency pairs are a concept that is at the core of all state-of-the-art automated termination provers for first-order term rewriting systems. In this paper, we extend this technique to higher-order rewriting and dependent types. We also extend to strong normalization and non-orthogonal rewrite systems previous results by Wahlstedt on one hand, and the first author on the other hand.