Refinement Types as Higher Order Dependency Pairs

Cody Roux 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Les types raffines permettent une analyse plus fine des programmes fonctionnels que les types simples. La methode des paires de dependance est une technique puissante utilisee pour montrer la terminaison. Cependant cette derniere n'as pas encore etee generalisee a la reecriture d'ordre superieure de maniere satisfaisante. Nous faisant l'observation suivante: une variete de types raffines peut etre tilisee pour proceder a une analyse de dependence des systemes de reecriture d'ordre superieurs. Nous donnons un critere de terminaison a base de ces types, et prouvons la correction du critere.
Type de document :
Rapport
[Research Report] 2011, pp.19
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00552046
Contributeur : Cody Roux <>
Soumis le : lundi 24 janvier 2011 - 17:20:55
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : lundi 25 avril 2011 - 03:23:12

Fichiers

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

Identifiants

  • HAL Id : inria-00552046, version 2
  • ARXIV : 1101.0968

Collections

Citation

Cody Roux. Refinement Types as Higher Order Dependency Pairs. [Research Report] 2011, pp.19. 〈inria-00552046v2〉

Partager

Métriques

Consultations de la notice

256

Téléchargements de fichiers

101