A type-based termination criterion for dependently-typed higher-order rewrite systems

Frédéric Blanqui 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Several authors devised type-based termination criteria for ML-like languages allowing non-structural recursive calls. We extend these works to general rewriting and dependent types, hence providing a powerful termination criterion for the combination of rewriting and beta-reduction in the Calculus of Constructions.
Type de document :
Communication dans un congrès
15th International Conference on Rewriting Techniques and Applications - RTA'04, 2004, Aachen, Germany. 2004
Liste complète des métadonnées

https://hal.inria.fr/inria-00100254
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 11 octobre 2006 - 12:05:24
Dernière modification le : jeudi 8 février 2018 - 11:32:01
Document(s) archivé(s) le : mardi 6 avril 2010 - 01:12:32

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui. A type-based termination criterion for dependently-typed higher-order rewrite systems. 15th International Conference on Rewriting Techniques and Applications - RTA'04, 2004, Aachen, Germany. 2004. 〈inria-00100254〉

Partager

Métriques

Consultations de la notice

168

Téléchargements de fichiers

77