Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Logic in Computer Science
2020-07-16 v2
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 resultsby 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.
Keywords
Cite
@article{arxiv.1906.11649,
title = {Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting},
author = {Frédéric Blanqui and Guillaume Genestier and Olivier Hermant},
journal= {arXiv preprint arXiv:1906.11649},
year = {2020}
}
Comments
FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany