Termination of dependently typed rewrite rules

Abstract : Our interest is in automated termination proofs of higher-order rewrite rules in presence of dependent types modulo a theory T on base types. We first describe an original transformation to a type discipline without type dependencies which preserves non-termination. Since the user must reason on expressions of the transformed language, we then introduce an extension of the computability path ordering CPO for comparing dependently typed expressions named DCPO. Using the previous result, we show that DCPO is a well-founded order, behaving well in practice.
Type de document :
Communication dans un congrès
Proc. TLCA 2015, Jul 2015, Varsaw, Poland. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, LIPIcs (38), 2015, 〈10.4230/LIPIcs.TLCA.2015.x〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01239083
Contributeur : Jean-Pierre Jouannaud <>
Soumis le : lundi 7 décembre 2015 - 13:45:33
Dernière modification le : jeudi 11 janvier 2018 - 06:19:44
Document(s) archivé(s) le : samedi 29 avril 2017 - 10:07:29

Fichier

TLCA.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Jean-Pierre Jouannaud, Jian-Qi Li. Termination of dependently typed rewrite rules. Proc. TLCA 2015, Jul 2015, Varsaw, Poland. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, LIPIcs (38), 2015, 〈10.4230/LIPIcs.TLCA.2015.x〉. 〈hal-01239083〉

Partager

Métriques

Consultations de la notice

105

Téléchargements de fichiers

53