Skip to Main content Skip to Navigation
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 metadatas

https://hal.inria.fr/hal-01943941
Contributor : Frédéric Blanqui <>
Submitted on : Tuesday, October 15, 2019 - 1:39:38 PM
Last modification on : Thursday, September 24, 2020 - 4:36:04 PM

Files

main.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

148

Files downloads

574