Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Journal articles

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 
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Monday, September 26, 2011 - 3:42:34 AM
Last modification on : Tuesday, July 5, 2022 - 8:38:58 AM
Long-term archiving on: : Tuesday, December 27, 2011 - 2:20:06 AM


Files produced by the author(s)


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



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⟩



Record views


Files downloads