Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.9
URN: urn:nbn:de:0030-drops-105167
URL: https://drops.dagstuhl.de/opus/volltexte/2019/10516/
Blanqui, Frédéric ; Genestier, Guillaume ; Hermant, Olivier
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
| pdf-format: |
|
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: | 18.06.2019 |
