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

Keiichirou Kusakari 1 Yasuo Isogai 1 Masahiko Sakai 1 Frédéric Blanqui 2
1 Sakabe-Sakai Laboratory
2 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : 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.
Keywords : higher-order rewriting lambda-calculus termination dependency pairs
Type de document :
Article dans une revue
IEICE Transactions on Information and Systems, Institute of Electronics, Information and Communication Engineers, 2009
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00397820
Contributeur : Frédéric Blanqui <>
Soumis le : lundi 26 septembre 2011 - 03:42:34
Dernière modification le : mercredi 10 octobre 2018 - 14:28:10
Document(s) archivé(s) le : mardi 27 décembre 2011 - 02:20:06

Fichiers

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

Identifiants

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

Collections

INRIA | LIAMA | CIRAD | INRA | INRIA-ROCQ

Citation

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, Institute of Electronics, Information and Communication Engineers, 2009. 〈inria-00397820〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

404

Téléchargements de fichiers

145

Contact


archive-ouverte@inria.fr