Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
| Autor: | Blanqui, Frédéric, Genestier, Guillaume, Hermant, Olivier |
|---|---|
| Jazyk: | angličtina |
| Předmět: |
000 Computer science
knowledge general works 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Computer Science 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages 020207 software engineering 0102 computer and information sciences 02 engineering and technology 01 natural sciences |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|