Blanqui, Frédéric ;
Genestier, Guillaume ;
Hermant, Olivier
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.
BibTeX - Entry
@InProceedings{blanqui_et_al:LIPIcs:2019:10516,
author = {Fr{\'e}d{\'e}ric Blanqui and Guillaume Genestier and Olivier Hermant},
title = {{Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting}},
booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
pages = {9:1--9:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-107-8},
ISSN = {1868-8969},
year = {2019},
volume = {131},
editor = {Herman Geuvers},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10516},
URN = {urn:nbn:de:0030-drops-105167},
doi = {10.4230/LIPIcs.FSCD.2019.9},
annote = {Keywords: termination, higher-order rewriting, dependent types, dependency pairs}
}
|
Keywords: |
|
termination, higher-order rewriting, dependent types, dependency pairs |
|
Seminar: |
|
4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
|
|
Issue date: |
|
2019 |
|
Date of publication: |
|
2019 |
2019
