On lexicographic termination ordering with space bound certifications
Identifieur interne :
000884 ( PascalFrancis/Corpus );
précédent :
000883;
suivant :
000885
On lexicographic termination ordering with space bound certifications
Auteurs : Guillaume Bonfante ;
Jean-Yves Marion ;
Jean-Yves MoyenSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2001.
RBID : Pascal:02-0191272
Descripteurs français
English descriptors
Abstract
We propose a method to analyse the program space complexity, based on termination orderings. This method can be implemented to certify the runspace of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by Lexicographic Path Ordering and admit a polynomial quasi-interpretation, is exactly the class of functions computable in polynomial space.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
| pA |
| A01 | 01 | 1 | | @0 0302-9743 |
|---|
| A05 | | | | @2 2244 |
|---|
| A08 | 01 | 1 | ENG | @1 On lexicographic termination ordering with space bound certifications |
|---|
| A09 | 01 | 1 | ENG | @1 PSI : perspectives of systems informatics : Novosibirsk, 2-6 July 2001, revised papers |
|---|
| A11 | 01 | 1 | | @1 BONFANTE (Guillaume) |
|---|
| A11 | 02 | 1 | | @1 MARION (Jean-Yves) |
|---|
| A11 | 03 | 1 | | @1 MOYEN (Jean-Yves) |
|---|
| A12 | 01 | 1 | | @1 BJORNER (Dines) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 BROY (Manfred) @9 ed. |
|---|
| A12 | 03 | 1 | | @1 ZAMULIN (Alexandre V.) @9 ed. |
|---|
| A14 | 01 | | | @1 Loria, Calligramme project, B.P. 239 @2 54506 Vandœuvre-lès-Nancy @3 FRA @Z 1 aut. @Z 2 aut. @Z 3 aut. |
|---|
| A20 | | | | @1 482-493 |
|---|
| A21 | | | | @1 2001 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-43075-X |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000097056000460 |
|---|
| A44 | | | | @0 0000 @1 © 2002 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 23 ref. |
|---|
| A47 | 01 | 1 | | @0 02-0191272 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Lecture notes in computer science |
|---|
| A66 | 01 | | | @0 DEU |
|---|
| C01 | 01 | | ENG | @0 We propose a method to analyse the program space complexity, based on termination orderings. This method can be implemented to certify the runspace of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by Lexicographic Path Ordering and admit a polynomial quasi-interpretation, is exactly the class of functions computable in polynomial space. |
|---|
| C02 | 01 | X | | @0 001D02A07 |
|---|
| C03 | 01 | X | FRE | @0 Fonction polynomiale @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Polynomial function @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Función polinomial @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Complexité programme @5 02 |
|---|
| C03 | 02 | X | ENG | @0 Program complexity @5 02 |
|---|
| C03 | 02 | X | SPA | @0 Complejidad programa @5 02 |
|---|
| C03 | 03 | X | FRE | @0 Certification @5 03 |
|---|
| C03 | 03 | X | ENG | @0 Certification @5 03 |
|---|
| C03 | 03 | X | SPA | @0 Certificación @5 03 |
|---|
| C03 | 04 | X | FRE | @0 Langage ordre 1 @5 04 |
|---|
| C03 | 04 | X | ENG | @0 First order language @5 04 |
|---|
| C03 | 04 | X | SPA | @0 Lenguaje orden 1 @5 04 |
|---|
| C03 | 05 | X | FRE | @0 Programmation fonctionnelle @5 05 |
|---|
| C03 | 05 | X | ENG | @0 Functional programming @5 05 |
|---|
| C03 | 05 | X | SPA | @0 Programación funcional @5 05 |
|---|
| C03 | 06 | X | FRE | @0 Analyse programme @5 06 |
|---|
| C03 | 06 | X | ENG | @0 Program analysis @5 06 |
|---|
| C03 | 06 | X | SPA | @0 Análisis programa @5 06 |
|---|
| C03 | 07 | X | FRE | @0 Relation ordre @5 07 |
|---|
| C03 | 07 | X | ENG | @0 Ordering @5 07 |
|---|
| C03 | 07 | X | SPA | @0 Relación orden @5 07 |
|---|
| C03 | 08 | X | FRE | @0 Ordre lexicographique @5 08 |
|---|
| C03 | 08 | X | ENG | @0 Lexicographic order @5 08 |
|---|
| C03 | 08 | X | SPA | @0 Orden lexicográfico @5 08 |
|---|
| N21 | | | | @1 112 |
|---|
| N82 | | | | @1 PSI |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International Andrei Ershov Memorial conference @2 4 @3 Novosibirsk RUS @4 2001-06-02 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 02-0191272 INIST |
|---|
| ET : | On lexicographic termination ordering with space bound certifications |
|---|
| AU : | BONFANTE (Guillaume); MARION (Jean-Yves); MOYEN (Jean-Yves); BJORNER (Dines); BROY (Manfred); ZAMULIN (Alexandre V.) |
|---|
| AF : | Loria, Calligramme project, B.P. 239/54506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut., 3 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2001; Vol. 2244; Pp. 482-493; Bibl. 23 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | We propose a method to analyse the program space complexity, based on termination orderings. This method can be implemented to certify the runspace of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by Lexicographic Path Ordering and admit a polynomial quasi-interpretation, is exactly the class of functions computable in polynomial space. |
|---|
| CC : | 001D02A07 |
|---|
| FD : | Fonction polynomiale; Complexité programme; Certification; Langage ordre 1; Programmation fonctionnelle; Analyse programme; Relation ordre; Ordre lexicographique |
|---|
| ED : | Polynomial function; Program complexity; Certification; First order language; Functional programming; Program analysis; Ordering; Lexicographic order |
|---|
| SD : | Función polinomial; Complejidad programa; Certificación; Lenguaje orden 1; Programación funcional; Análisis programa; Relación orden; Orden lexicográfico |
|---|
| LO : | INIST-16343.354000097056000460 |
|---|
| ID : | 02-0191272 |
|---|
Links to Exploration step
Pascal:02-0191272
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">On lexicographic termination ordering with space bound certifications</title>
<author><name sortKey="Bonfante, Guillaume" sort="Bonfante, Guillaume" uniqKey="Bonfante G" first="Guillaume" last="Bonfante">Guillaume Bonfante</name>
<affiliation><inist:fA14 i1="01"><s1>Loria, Calligramme project, B.P. 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
<affiliation><inist:fA14 i1="01"><s1>Loria, Calligramme project, B.P. 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><author><name sortKey="Moyen, Jean Yves" sort="Moyen, Jean Yves" uniqKey="Moyen J" first="Jean-Yves" last="Moyen">Jean-Yves Moyen</name>
<affiliation><inist:fA14 i1="01"><s1>Loria, Calligramme project, B.P. 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">02-0191272</idno>
<date when="2001">2001</date>
<idno type="stanalyst">PASCAL 02-0191272 INIST</idno>
<idno type="RBID">Pascal:02-0191272</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000884</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">On lexicographic termination ordering with space bound certifications</title>
<author><name sortKey="Bonfante, Guillaume" sort="Bonfante, Guillaume" uniqKey="Bonfante G" first="Guillaume" last="Bonfante">Guillaume Bonfante</name>
<affiliation><inist:fA14 i1="01"><s1>Loria, Calligramme project, B.P. 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
<affiliation><inist:fA14 i1="01"><s1>Loria, Calligramme project, B.P. 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><author><name sortKey="Moyen, Jean Yves" sort="Moyen, Jean Yves" uniqKey="Moyen J" first="Jean-Yves" last="Moyen">Jean-Yves Moyen</name>
<affiliation><inist:fA14 i1="01"><s1>Loria, Calligramme project, B.P. 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2001">2001</date>
</imprint><seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Certification</term>
<term>First order language</term>
<term>Functional programming</term>
<term>Lexicographic order</term>
<term>Ordering</term>
<term>Polynomial function</term>
<term>Program analysis</term>
<term>Program complexity</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Fonction polynomiale</term>
<term>Complexité programme</term>
<term>Certification</term>
<term>Langage ordre 1</term>
<term>Programmation fonctionnelle</term>
<term>Analyse programme</term>
<term>Relation ordre</term>
<term>Ordre lexicographique</term>
</keywords><front><div type="abstract" xml:lang="en">We propose a method to analyse the program space complexity, based on termination orderings. This method can be implemented to certify the runspace of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by Lexicographic Path Ordering and admit a polynomial quasi-interpretation, is exactly the class of functions computable in polynomial space.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>2244</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>On lexicographic termination ordering with space bound certifications</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>PSI : perspectives of systems informatics : Novosibirsk, 2-6 July 2001, revised papers</s1>
</fA09><fA11 i1="01" i2="1"><s1>BONFANTE (Guillaume)</s1>
</fA11><fA11 i1="02" i2="1"><s1>MARION (Jean-Yves)</s1>
</fA11><fA11 i1="03" i2="1"><s1>MOYEN (Jean-Yves)</s1>
</fA11><fA12 i1="01" i2="1"><s1>BJORNER (Dines)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>BROY (Manfred)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="03" i2="1"><s1>ZAMULIN (Alexandre V.)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>Loria, Calligramme project, B.P. 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</fA14><fA20><s1>482-493</s1>
</fA20><fA21><s1>2001</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-43075-X</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000097056000460</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2002 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>23 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>02-0191272</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64><fA66 i1="01"><s0>DEU</s0>
</fA66><fC01 i1="01" l="ENG"><s0>We propose a method to analyse the program space complexity, based on termination orderings. This method can be implemented to certify the runspace of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by Lexicographic Path Ordering and admit a polynomial quasi-interpretation, is exactly the class of functions computable in polynomial space.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A07</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Fonction polynomiale</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Polynomial function</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Función polinomial</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Complexité programme</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Program complexity</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Complejidad programa</s0>
<s5>02</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Certification</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Certification</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Certificación</s0>
<s5>03</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Langage ordre 1</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>First order language</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Lenguaje orden 1</s0>
<s5>04</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Programmation fonctionnelle</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Functional programming</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Programación funcional</s0>
<s5>05</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Analyse programme</s0>
<s5>06</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Program analysis</s0>
<s5>06</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Análisis programa</s0>
<s5>06</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Relation ordre</s0>
<s5>07</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Ordering</s0>
<s5>07</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Relación orden</s0>
<s5>07</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Ordre lexicographique</s0>
<s5>08</s5>
</fC03><fC03 i1="08" i2="X" l="ENG"><s0>Lexicographic order</s0>
<s5>08</s5>
</fC03><fC03 i1="08" i2="X" l="SPA"><s0>Orden lexicográfico</s0>
<s5>08</s5>
</fC03><fN21><s1>112</s1>
</fN21><fN82><s1>PSI</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>International Andrei Ershov Memorial conference </s1>
<s2>4</s2>
<s3>Novosibirsk RUS</s3>
<s4>2001-06-02</s4>
</fA30><server><NO>PASCAL 02-0191272 INIST</NO>
<ET>On lexicographic termination ordering with space bound certifications</ET>
<AU>BONFANTE (Guillaume); MARION (Jean-Yves); MOYEN (Jean-Yves); BJORNER (Dines); BROY (Manfred); ZAMULIN (Alexandre V.)</AU>
<AF>Loria, Calligramme project, B.P. 239/54506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut., 3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2001; Vol. 2244; Pp. 482-493; Bibl. 23 ref.</SO>
<LA>Anglais</LA>
<EA>We propose a method to analyse the program space complexity, based on termination orderings. This method can be implemented to certify the runspace of programs. We demonstrate that the class of functions computed by first order functional programs over free algebras which terminate by Lexicographic Path Ordering and admit a polynomial quasi-interpretation, is exactly the class of functions computable in polynomial space.</EA>
<CC>001D02A07</CC>
<FD>Fonction polynomiale; Complexité programme; Certification; Langage ordre 1; Programmation fonctionnelle; Analyse programme; Relation ordre; Ordre lexicographique</FD>
<ED>Polynomial function; Program complexity; Certification; First order language; Functional programming; Program analysis; Ordering; Lexicographic order</ED>
<SD>Función polinomial; Complejidad programa; Certificación; Lenguaje orden 1; Programación funcional; Análisis programa; Relación orden; Orden lexicográfico</SD>
<LO>INIST-16343.354000097056000460</LO>
<ID>02-0191272</ID>
</server>
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 000884 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000884 | 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:02-0191272
|texte= On lexicographic termination ordering with space bound certifications
}}
| 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 |  |
