Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue IEICE Transactions on Information and Systems Année : 2009

Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems

Keiichirou Kusakari
  • Fonction : Auteur
  • PersonId : 861355
Yasuo Isogai
  • Fonction : Auteur
  • PersonId : 861356
Masahiko Sakai
  • Fonction : Auteur
  • PersonId : 861357
Frédéric Blanqui

Résumé

Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include λ-abstraction but STRSs do not, we restructure the static dependency pair method to allow λ-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions.
Fichier principal
Vignette du fichier
main.pdf (205.94 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00397820 , version 1 (26-09-2011)

Identifiants

  • HAL Id : inria-00397820 , version 1
  • ARXIV : 1109.5468

Citer

Keiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, Frédéric Blanqui. Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems. IEICE Transactions on Information and Systems, 2009. ⟨inria-00397820⟩
189 Consultations
108 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More