InforLorV4, PascalFrancis, Corpus, bibRecord, 000219

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

Identifieur interne : 000219 ( PascalFrancis/Corpus ); précédent : 000218; suivant : 000220

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

Auteurs : Keiichirou Kusakari ; Yasuo Isogai ; Masahiko Sakai ; Frédéric Blanqui

Source :

IEICE transactions on information and systems [ 0916-8532 ] ; 2009.

RBID : Pascal:10-0210395

Descripteurs français

Pascal (Inist)
- Calculabilité, Système réécriture, Traitement donnée.

English descriptors

KwdEn :
- Computability, Data processing, Rewriting systems.

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.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A01	`01`	`1`		`@0 0916-8532`
A03		`1`		`@0 IEICE trans. inf. syst.`
A05				`@2 92`
A06				`@2 10`
A08	`01`	`1`	`ENG`	`@1 Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems`
A11	`01`	`1`		`@1 KUSAKARI (Keiichirou)`
A11	`02`	`1`		`@1 ISOGAI (Yasuo)`
A11	`03`	`1`		`@1 SAKAI (Masahiko)`
A11	`04`	`1`		`@1 BLANQUI (Frédéric)`
A14	`01`			`@1 Graduate School of Information Science, Nagoya Univ. @2 Nagoya-shi, 464-8601 @3 JPN @Z 1 aut. @Z 2 aut. @Z 3 aut.`
A14	`02`			`@1 INRIA & LORIA @3 FRA @Z 4 aut.`
A20				`@1 2007-2015`
A21				`@1 2009`
A23	`01`			`@0 ENG`
A43	`01`			`@1 INIST @2 7315E4 @5 354000181713490220`
A44				`@0 0000 @1 © 2010 INIST-CNRS. All rights reserved.`
A45				`@0 24 ref.`
A47	`01`	`1`		`@0 10-0210395`
A60				`@1 P`
A61				`@0 A`
A64	`01`	`1`		`@0 IEICE transactions on information and systems`
A66	`01`			`@0 GBR`
C01	`01`		`ENG`	@0 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.
C02	`01`	`X`		`@0 001D04A03`
C02	`02`	`X`		`@0 001D02B07B`
C03	`01`	`X`	`FRE`	`@0 Calculabilité @5 01`
C03	`01`	`X`	`ENG`	`@0 Computability @5 01`
C03	`01`	`X`	`SPA`	`@0 Calculabilidad @5 01`
C03	`02`	`3`	`FRE`	`@0 Système réécriture @5 02`
C03	`02`	`3`	`ENG`	`@0 Rewriting systems @5 02`
C03	`03`	`X`	`FRE`	`@0 Traitement donnée @5 03`
C03	`03`	`X`	`ENG`	`@0 Data processing @5 03`
C03	`03`	`X`	`SPA`	`@0 Tratamiento datos @5 03`
N21				`@1 144`

Format Inist (serveur)

NO :	PASCAL 10-0210395 INIST
ET :	Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems
AU :	KUSAKARI (Keiichirou); ISOGAI (Yasuo); SAKAI (Masahiko); BLANQUI (Frédéric)
AF :	Graduate School of Information Science, Nagoya Univ./Nagoya-shi, 464-8601/Japon (1 aut., 2 aut., 3 aut.); INRIA & LORIA/France (4 aut.)
DT :	Publication en série; Niveau analytique
SO :	IEICE transactions on information and systems; ISSN 0916-8532; Royaume-Uni; Da. 2009; Vol. 92; No. 10; Pp. 2007-2015; Bibl. 24 ref.
LA :	Anglais
EA :	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.
CC :	001D04A03; 001D02B07B
FD :	Calculabilité; Système réécriture; Traitement donnée
ED :	Computability; Rewriting systems; Data processing
SD :	Calculabilidad; Tratamiento datos
LO :	INIST-7315E4.354000181713490220
ID :	10-0210395

Links to Exploration step

Pascal:10-0210395

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems</title>
<author><name sortKey="Kusakari, Keiichirou" sort="Kusakari, Keiichirou" uniqKey="Kusakari K" first="Keiichirou" last="Kusakari">Keiichirou Kusakari</name>
<affiliation><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Isogai, Yasuo" sort="Isogai, Yasuo" uniqKey="Isogai Y" first="Yasuo" last="Isogai">Yasuo Isogai</name>
<affiliation><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Sakai, Masahiko" sort="Sakai, Masahiko" uniqKey="Sakai M" first="Masahiko" last="Sakai">Masahiko Sakai</name>
<affiliation><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation><inist:fA14 i1="02"><s1>INRIA & LORIA</s1>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">10-0210395</idno>
<date when="2009">2009</date>
<idno type="stanalyst">PASCAL 10-0210395 INIST</idno>
<idno type="RBID">Pascal:10-0210395</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000219</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems</title>
<author><name sortKey="Kusakari, Keiichirou" sort="Kusakari, Keiichirou" uniqKey="Kusakari K" first="Keiichirou" last="Kusakari">Keiichirou Kusakari</name>
<affiliation><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Isogai, Yasuo" sort="Isogai, Yasuo" uniqKey="Isogai Y" first="Yasuo" last="Isogai">Yasuo Isogai</name>
<affiliation><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Sakai, Masahiko" sort="Sakai, Masahiko" uniqKey="Sakai M" first="Masahiko" last="Sakai">Masahiko Sakai</name>
<affiliation><inist:fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation><inist:fA14 i1="02"><s1>INRIA & LORIA</s1>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">IEICE transactions on information and systems</title>
<title level="j" type="abbreviated">IEICE trans. inf. syst.</title>
<idno type="ISSN">0916-8532</idno>
<imprint><date when="2009">2009</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">IEICE transactions on information and systems</title>
<title level="j" type="abbreviated">IEICE trans. inf. syst.</title>
<idno type="ISSN">0916-8532</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Computability</term>
<term>Data processing</term>
<term>Rewriting systems</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Calculabilité</term>
<term>Système réécriture</term>
<term>Traitement donnée</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">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.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0916-8532</s0>
</fA01>
<fA03 i2="1"><s0>IEICE trans. inf. syst.</s0>
</fA03>
<fA05><s2>92</s2>
</fA05>
<fA06><s2>10</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems</s1>
</fA08>
<fA11 i1="01" i2="1"><s1>KUSAKARI (Keiichirou)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>ISOGAI (Yasuo)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>SAKAI (Masahiko)</s1>
</fA11>
<fA11 i1="04" i2="1"><s1>BLANQUI (Frédéric)</s1>
</fA11>
<fA14 i1="01"><s1>Graduate School of Information Science, Nagoya Univ.</s1>
<s2>Nagoya-shi, 464-8601</s2>
<s3>JPN</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>INRIA & LORIA</s1>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
</fA14>
<fA20><s1>2007-2015</s1>
</fA20>
<fA21><s1>2009</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>7315E4</s2>
<s5>354000181713490220</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2010 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>24 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>10-0210395</s0>
</fA47>
<fA60><s1>P</s1>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>IEICE transactions on information and systems</s0>
</fA64>
<fA66 i1="01"><s0>GBR</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>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.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D04A03</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02B07B</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Calculabilité</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Computability</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Calculabilidad</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="3" l="FRE"><s0>Système réécriture</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="3" l="ENG"><s0>Rewriting systems</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Traitement donnée</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Data processing</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Tratamiento datos</s0>
<s5>03</s5>
</fC03>
<fN21><s1>144</s1>
</fN21>
</pA>
</standard>
<server><NO>PASCAL 10-0210395 INIST</NO>
<ET>Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems</ET>
<AU>KUSAKARI (Keiichirou); ISOGAI (Yasuo); SAKAI (Masahiko); BLANQUI (Frédéric)</AU>
<AF>Graduate School of Information Science, Nagoya Univ./Nagoya-shi, 464-8601/Japon (1 aut., 2 aut., 3 aut.); INRIA & LORIA/France (4 aut.)</AF>
<DT>Publication en série; Niveau analytique</DT>
<SO>IEICE transactions on information and systems; ISSN 0916-8532; Royaume-Uni; Da. 2009; Vol. 92; No. 10; Pp. 2007-2015; Bibl. 24 ref.</SO>
<LA>Anglais</LA>
<EA>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.</EA>
<CC>001D04A03; 001D02B07B</CC>
<FD>Calculabilité; Système réécriture; Traitement donnée</FD>
<ED>Computability; Rewriting systems; Data processing</ED>
<SD>Calculabilidad; Tratamiento datos</SD>
<LO>INIST-7315E4.354000181713490220</LO>
<ID>10-0210395</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000219 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000219 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |type=    RBID
   |clé=     Pascal:10-0210395
   |texte=   Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

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

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

Source :

Descripteurs français

English descriptors

Abstract

Notice en format standard (ISO 2709)

Format Inist (serveur)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri