Refinement types as higher order dependency pairs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

Refinement types as higher order dependency pairs

Cody Roux
  • Fonction : Auteur
  • PersonId : 845905

Résumé

Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of rewrite systems; however its extension to higher-order rewrite systems is still the subject of active research. We observe that a variant of refinement types allows us to express a form of higher-order dependency pair method: from the rewrite system labeled with typing information, we build a type-level approximated dependency graph, and describe a type level embedding-order. We describe a syntactic termination criterion involving the graph and the order, and prove our main result: if the graph passes the criterion, then every well-typed term is strongly normalizing.
Nous modifions l'approche classique de la terminaison a base de tailles et montrons que le système modifie permet une analyse fine du flot de contrôle dans un langage d'ordre supérieur. Ceci nous permet de construire un graphe, dit graphe de dépendance approxime, et nous pouvons montrer qu'un critère syntaxique sur ce graphe suffit a montrer la terminaison de tout terme bien type.
Fichier principal
Vignette du fichier
roux_ref_dp.pdf (272.82 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00598567 , version 1 (06-06-2011)

Identifiants

  • HAL Id : inria-00598567 , version 1

Citer

Cody Roux. Refinement types as higher order dependency pairs. RTA'11 - 22nd International Conference on Rewriting Techniques and Applications, May 2011, Novi Sad, Serbia. pp.299-312. ⟨inria-00598567⟩
56 Consultations
54 Téléchargements

Partager

Gmail Facebook X LinkedIn More