Skip to Main content Skip to Navigation
New interface
Conference papers

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

Abstract : Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. This extends previous results by Wahlstedt on the one hand and the first author on the other hand to strong normalization and non-orthogonal rewriting systems. This new criterion is implemented in the type-checker Dedukti.
Document type :
Conference papers
Complete list of metadata
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Tuesday, October 15, 2019 - 1:39:38 PM
Last modification on : Tuesday, October 25, 2022 - 4:16:15 PM


Files produced by the author(s)



Frédéric Blanqui, Guillaume Genestier, Olivier Hermant. Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting. FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨10.4230/LIPIcs.FSCD.2019.9⟩. ⟨hal-01943941v4⟩



Record views


Files downloads