InforLorV4, PascalFrancis, Corpus, bibRecord, 000516

Selecting theories and recursive protocols

Identifieur interne : 000516 ( PascalFrancis/Corpus ); précédent : 000515; suivant : 000517

Selecting theories and recursive protocols

Auteurs : Tomasz Truderung

Source :

Lecture notes in computer science [ 0302-9743 ] ; 2005.

RBID : Pascal:05-0410073

Descripteurs français

Pascal (Inist)
- Simultanéité informatique, Système réparti, Méthode récursive, Décidabilité, Protocole transmission, Cryptographie, Automate arbre, Système réécriture, Réécriture, Test égalité, Architecture basée modèle, Modélisation, ., Indécidabilité.

English descriptors

KwdEn :
- Concurrency, Cryptography, Decidability, Distributed system, Equality test, Model driven architecture, Modeling, Recursive method, Rewriting, Rewriting systems, Transmission protocol, Tree automaton, Undecidability.

Abstract

Many decidability results are known for non-recursive cryptographic protocols, where the protocol steps can be expressed by simple rewriting rules. Recently, a tree transducer-based model was proposed for recursive protocols, where the protocol steps involve some kind of recursive computations. This model has, however, some limitations: (1) rules are assumed to have linear lefthand sides (so no equality tests can be performed), (2) only finite amount of information can be conveyed from one receive-send action to the next ones. It has been proven that, in this model, relaxing these assumptions leads to undecidability. In this paper, we propose a formalism, called selecting theories, which extends the standard non-recursive term rewriting model and allows participants to compare and store arbitrary messages. This formalism can model recursive protocols, where participants, in each protocol step, are able to send a number of messages unbounded w.r.t. the size of the protocol. We prove that insecurity of protocols with selecting theories is decidable in NEXPTIME.

Notice en format standard (ISO 2709)

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

A01	`01`	`1`		`@0 0302-9743`
A05				`@2 3653`
A08	`01`	`1`	`ENG`	`@1 Selecting theories and recursive protocols`
A09	`01`	`1`	`ENG`	`@1 CONCUR 2005 : concurrency theory : San Francisco CA? 23-26 August 2005`
A11	`01`	`1`		`@1 TRUDERUNG (Tomasz)`
A12	`01`	`1`		`@1 ABADI (Martin) @9 ed.`
A12	`02`	`1`		`@1 ALFARO (Luca de) @9 ed.`
A14	`01`			`@1 LORIA-INRIA-Lorraine @3 FRA @Z 1 aut.`
A14	`02`			`@1 Institute of Computer Science, Wroclaw University @3 POL @Z 1 aut.`
A20				`@1 217-232`
A21				`@1 2005`
A23	`01`			`@0 ENG`
A26	`01`			`@0 3-540-28309-9`
A43	`01`			`@1 INIST @2 16343 @5 354000124408310150`
A44				`@0 0000 @1 © 2005 INIST-CNRS. All rights reserved.`
A45				`@0 17 ref.`
A47	`01`	`1`		`@0 05-0410073`
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 Many decidability results are known for non-recursive cryptographic protocols, where the protocol steps can be expressed by simple rewriting rules. Recently, a tree transducer-based model was proposed for recursive protocols, where the protocol steps involve some kind of recursive computations. This model has, however, some limitations: (1) rules are assumed to have linear lefthand sides (so no equality tests can be performed), (2) only finite amount of information can be conveyed from one receive-send action to the next ones. It has been proven that, in this model, relaxing these assumptions leads to undecidability. In this paper, we propose a formalism, called selecting theories, which extends the standard non-recursive term rewriting model and allows participants to compare and store arbitrary messages. This formalism can model recursive protocols, where participants, in each protocol step, are able to send a number of messages unbounded w.r.t. the size of the protocol. We prove that insecurity of protocols with selecting theories is decidable in NEXPTIME.
C02	`01`	`X`		`@0 001D02B07C`
C02	`02`	`X`		`@0 001D04A04E`
C02	`03`	`X`		`@0 001D02B04`
C03	`01`	`X`	`FRE`	`@0 Simultanéité informatique @5 01`
C03	`01`	`X`	`ENG`	`@0 Concurrency @5 01`
C03	`01`	`X`	`SPA`	`@0 Simultaneidad informatica @5 01`
C03	`02`	`X`	`FRE`	`@0 Système réparti @5 02`
C03	`02`	`X`	`ENG`	`@0 Distributed system @5 02`
C03	`02`	`X`	`SPA`	`@0 Sistema repartido @5 02`
C03	`03`	`X`	`FRE`	`@0 Méthode récursive @5 06`
C03	`03`	`X`	`ENG`	`@0 Recursive method @5 06`
C03	`03`	`X`	`SPA`	`@0 Método recursivo @5 06`
C03	`04`	`X`	`FRE`	`@0 Décidabilité @5 07`
C03	`04`	`X`	`ENG`	`@0 Decidability @5 07`
C03	`04`	`X`	`SPA`	`@0 Decidibilidad @5 07`
C03	`05`	`X`	`FRE`	`@0 Protocole transmission @5 08`
C03	`05`	`X`	`ENG`	`@0 Transmission protocol @5 08`
C03	`05`	`X`	`SPA`	`@0 Protocolo transmisión @5 08`
C03	`06`	`X`	`FRE`	`@0 Cryptographie @5 09`
C03	`06`	`X`	`ENG`	`@0 Cryptography @5 09`
C03	`06`	`X`	`SPA`	`@0 Criptografía @5 09`
C03	`07`	`X`	`FRE`	`@0 Automate arbre @5 10`
C03	`07`	`X`	`ENG`	`@0 Tree automaton @5 10`
C03	`07`	`X`	`SPA`	`@0 Autómata árbol @5 10`
C03	`08`	`3`	`FRE`	`@0 Système réécriture @5 11`
C03	`08`	`3`	`ENG`	`@0 Rewriting systems @5 11`
C03	`09`	`X`	`FRE`	`@0 Réécriture @5 18`
C03	`09`	`X`	`ENG`	`@0 Rewriting @5 18`
C03	`09`	`X`	`SPA`	`@0 Reescritura @5 18`
C03	`10`	`X`	`FRE`	`@0 Test égalité @5 19`
C03	`10`	`X`	`ENG`	`@0 Equality test @5 19`
C03	`10`	`X`	`SPA`	`@0 Test igualdad @5 19`
C03	`11`	`X`	`FRE`	`@0 Architecture basée modèle @5 23`
C03	`11`	`X`	`ENG`	`@0 Model driven architecture @5 23`
C03	`11`	`X`	`SPA`	`@0 Arquitectura basada modelo @5 23`
C03	`12`	`X`	`FRE`	`@0 Modélisation @5 24`
C03	`12`	`X`	`ENG`	`@0 Modeling @5 24`
C03	`12`	`X`	`SPA`	`@0 Modelización @5 24`
C03	`13`	`X`	`FRE`	`@0 . @4 INC @5 82`
C03	`14`	`X`	`FRE`	`@0 Indécidabilité @4 CD @5 96`
C03	`14`	`X`	`ENG`	`@0 Undecidability @4 CD @5 96`
C03	`14`	`X`	`SPA`	`@0 Indecidibilidad @4 CD @5 96`
N21				`@1 283`
N44	`01`			`@1 OTO`
N82				`@1 OTO`

A30	`01`	`1`	`ENG`	`@1 International conference on concurrence theoryd @2 16 @3 San Francisco CA USA @4 2005-08-23`

Format Inist (serveur)

NO :	PASCAL 05-0410073 INIST
ET :	Selecting theories and recursive protocols
AU :	TRUDERUNG (Tomasz); ABADI (Martin); ALFARO (Luca de)
AF :	LORIA-INRIA-Lorraine/France (1 aut.); Institute of Computer Science, Wroclaw University/Pologne (1 aut.)
DT :	Publication en série; Congrès; Niveau analytique
SO :	Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2005; Vol. 3653; Pp. 217-232; Bibl. 17 ref.
LA :	Anglais
EA :	Many decidability results are known for non-recursive cryptographic protocols, where the protocol steps can be expressed by simple rewriting rules. Recently, a tree transducer-based model was proposed for recursive protocols, where the protocol steps involve some kind of recursive computations. This model has, however, some limitations: (1) rules are assumed to have linear lefthand sides (so no equality tests can be performed), (2) only finite amount of information can be conveyed from one receive-send action to the next ones. It has been proven that, in this model, relaxing these assumptions leads to undecidability. In this paper, we propose a formalism, called selecting theories, which extends the standard non-recursive term rewriting model and allows participants to compare and store arbitrary messages. This formalism can model recursive protocols, where participants, in each protocol step, are able to send a number of messages unbounded w.r.t. the size of the protocol. We prove that insecurity of protocols with selecting theories is decidable in NEXPTIME.
CC :	001D02B07C; 001D04A04E; 001D02B04
FD :	Simultanéité informatique; Système réparti; Méthode récursive; Décidabilité; Protocole transmission; Cryptographie; Automate arbre; Système réécriture; Réécriture; Test égalité; Architecture basée modèle; Modélisation; .; Indécidabilité
ED :	Concurrency; Distributed system; Recursive method; Decidability; Transmission protocol; Cryptography; Tree automaton; Rewriting systems; Rewriting; Equality test; Model driven architecture; Modeling; Undecidability
SD :	Simultaneidad informatica; Sistema repartido; Método recursivo; Decidibilidad; Protocolo transmisión; Criptografía; Autómata árbol; Reescritura; Test igualdad; Arquitectura basada modelo; Modelización; Indecidibilidad
LO :	INIST-16343.354000124408310150
ID :	05-0410073

Links to Exploration step

Pascal:05-0410073

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Selecting theories and recursive protocols</title>
<author><name sortKey="Truderung, Tomasz" sort="Truderung, Tomasz" uniqKey="Truderung T" first="Tomasz" last="Truderung">Tomasz Truderung</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Lorraine</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="02"><s1>Institute of Computer Science, Wroclaw University</s1>
<s3>POL</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">05-0410073</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 05-0410073 INIST</idno>
<idno type="RBID">Pascal:05-0410073</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000516</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Selecting theories and recursive protocols</title>
<author><name sortKey="Truderung, Tomasz" sort="Truderung, Tomasz" uniqKey="Truderung T" first="Tomasz" last="Truderung">Tomasz Truderung</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA-INRIA-Lorraine</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="02"><s1>Institute of Computer Science, Wroclaw University</s1>
<s3>POL</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2005">2005</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Concurrency</term>
<term>Cryptography</term>
<term>Decidability</term>
<term>Distributed system</term>
<term>Equality test</term>
<term>Model driven architecture</term>
<term>Modeling</term>
<term>Recursive method</term>
<term>Rewriting</term>
<term>Rewriting systems</term>
<term>Transmission protocol</term>
<term>Tree automaton</term>
<term>Undecidability</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Simultanéité informatique</term>
<term>Système réparti</term>
<term>Méthode récursive</term>
<term>Décidabilité</term>
<term>Protocole transmission</term>
<term>Cryptographie</term>
<term>Automate arbre</term>
<term>Système réécriture</term>
<term>Réécriture</term>
<term>Test égalité</term>
<term>Architecture basée modèle</term>
<term>Modélisation</term>
<term>.</term>
<term>Indécidabilité</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Many decidability results are known for non-recursive cryptographic protocols, where the protocol steps can be expressed by simple rewriting rules. Recently, a tree transducer-based model was proposed for recursive protocols, where the protocol steps involve some kind of recursive computations. This model has, however, some limitations: (1) rules are assumed to have linear lefthand sides (so no equality tests can be performed), (2) only finite amount of information can be conveyed from one receive-send action to the next ones. It has been proven that, in this model, relaxing these assumptions leads to undecidability. In this paper, we propose a formalism, called selecting theories, which extends the standard non-recursive term rewriting model and allows participants to compare and store arbitrary messages. This formalism can model recursive protocols, where participants, in each protocol step, are able to send a number of messages unbounded w.r.t. the size of the protocol. We prove that insecurity of protocols with selecting theories is decidable in NEXPTIME.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01>
<fA05><s2>3653</s2>
</fA05>
<fA08 i1="01" i2="1" l="ENG"><s1>Selecting theories and recursive protocols</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>CONCUR 2005 : concurrency theory : San Francisco CA? 23-26 August 2005</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>TRUDERUNG (Tomasz)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>ABADI (Martin)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>ALFARO (Luca de)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>LORIA-INRIA-Lorraine</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>Institute of Computer Science, Wroclaw University</s1>
<s3>POL</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA20><s1>217-232</s1>
</fA20>
<fA21><s1>2005</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA26 i1="01"><s0>3-540-28309-9</s0>
</fA26>
<fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000124408310150</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2005 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>17 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>05-0410073</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<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>Many decidability results are known for non-recursive cryptographic protocols, where the protocol steps can be expressed by simple rewriting rules. Recently, a tree transducer-based model was proposed for recursive protocols, where the protocol steps involve some kind of recursive computations. This model has, however, some limitations: (1) rules are assumed to have linear lefthand sides (so no equality tests can be performed), (2) only finite amount of information can be conveyed from one receive-send action to the next ones. It has been proven that, in this model, relaxing these assumptions leads to undecidability. In this paper, we propose a formalism, called selecting theories, which extends the standard non-recursive term rewriting model and allows participants to compare and store arbitrary messages. This formalism can model recursive protocols, where participants, in each protocol step, are able to send a number of messages unbounded w.r.t. the size of the protocol. We prove that insecurity of protocols with selecting theories is decidable in NEXPTIME.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02B07C</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D04A04E</s0>
</fC02>
<fC02 i1="03" i2="X"><s0>001D02B04</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Simultanéité informatique</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Concurrency</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Simultaneidad informatica</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Système réparti</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Distributed system</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Sistema repartido</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Méthode récursive</s0>
<s5>06</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Recursive method</s0>
<s5>06</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Método recursivo</s0>
<s5>06</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Décidabilité</s0>
<s5>07</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Decidability</s0>
<s5>07</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Decidibilidad</s0>
<s5>07</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Protocole transmission</s0>
<s5>08</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Transmission protocol</s0>
<s5>08</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Protocolo transmisión</s0>
<s5>08</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Cryptographie</s0>
<s5>09</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Cryptography</s0>
<s5>09</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Criptografía</s0>
<s5>09</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Automate arbre</s0>
<s5>10</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Tree automaton</s0>
<s5>10</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA"><s0>Autómata árbol</s0>
<s5>10</s5>
</fC03>
<fC03 i1="08" i2="3" l="FRE"><s0>Système réécriture</s0>
<s5>11</s5>
</fC03>
<fC03 i1="08" i2="3" l="ENG"><s0>Rewriting systems</s0>
<s5>11</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Réécriture</s0>
<s5>18</s5>
</fC03>
<fC03 i1="09" i2="X" l="ENG"><s0>Rewriting</s0>
<s5>18</s5>
</fC03>
<fC03 i1="09" i2="X" l="SPA"><s0>Reescritura</s0>
<s5>18</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>Test égalité</s0>
<s5>19</s5>
</fC03>
<fC03 i1="10" i2="X" l="ENG"><s0>Equality test</s0>
<s5>19</s5>
</fC03>
<fC03 i1="10" i2="X" l="SPA"><s0>Test igualdad</s0>
<s5>19</s5>
</fC03>
<fC03 i1="11" i2="X" l="FRE"><s0>Architecture basée modèle</s0>
<s5>23</s5>
</fC03>
<fC03 i1="11" i2="X" l="ENG"><s0>Model driven architecture</s0>
<s5>23</s5>
</fC03>
<fC03 i1="11" i2="X" l="SPA"><s0>Arquitectura basada modelo</s0>
<s5>23</s5>
</fC03>
<fC03 i1="12" i2="X" l="FRE"><s0>Modélisation</s0>
<s5>24</s5>
</fC03>
<fC03 i1="12" i2="X" l="ENG"><s0>Modeling</s0>
<s5>24</s5>
</fC03>
<fC03 i1="12" i2="X" l="SPA"><s0>Modelización</s0>
<s5>24</s5>
</fC03>
<fC03 i1="13" i2="X" l="FRE"><s0>.</s0>
<s4>INC</s4>
<s5>82</s5>
</fC03>
<fC03 i1="14" i2="X" l="FRE"><s0>Indécidabilité</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="14" i2="X" l="ENG"><s0>Undecidability</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="14" i2="X" l="SPA"><s0>Indecidibilidad</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fN21><s1>283</s1>
</fN21>
<fN44 i1="01"><s1>OTO</s1>
</fN44>
<fN82><s1>OTO</s1>
</fN82>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>International conference on concurrence theoryd</s1>
<s2>16</s2>
<s3>San Francisco CA USA</s3>
<s4>2005-08-23</s4>
</fA30>
</pR>
</standard>
<server><NO>PASCAL 05-0410073 INIST</NO>
<ET>Selecting theories and recursive protocols</ET>
<AU>TRUDERUNG (Tomasz); ABADI (Martin); ALFARO (Luca de)</AU>
<AF>LORIA-INRIA-Lorraine/France (1 aut.); Institute of Computer Science, Wroclaw University/Pologne (1 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2005; Vol. 3653; Pp. 217-232; Bibl. 17 ref.</SO>
<LA>Anglais</LA>
<EA>Many decidability results are known for non-recursive cryptographic protocols, where the protocol steps can be expressed by simple rewriting rules. Recently, a tree transducer-based model was proposed for recursive protocols, where the protocol steps involve some kind of recursive computations. This model has, however, some limitations: (1) rules are assumed to have linear lefthand sides (so no equality tests can be performed), (2) only finite amount of information can be conveyed from one receive-send action to the next ones. It has been proven that, in this model, relaxing these assumptions leads to undecidability. In this paper, we propose a formalism, called selecting theories, which extends the standard non-recursive term rewriting model and allows participants to compare and store arbitrary messages. This formalism can model recursive protocols, where participants, in each protocol step, are able to send a number of messages unbounded w.r.t. the size of the protocol. We prove that insecurity of protocols with selecting theories is decidable in NEXPTIME.</EA>
<CC>001D02B07C; 001D04A04E; 001D02B04</CC>
<FD>Simultanéité informatique; Système réparti; Méthode récursive; Décidabilité; Protocole transmission; Cryptographie; Automate arbre; Système réécriture; Réécriture; Test égalité; Architecture basée modèle; Modélisation; .; Indécidabilité</FD>
<ED>Concurrency; Distributed system; Recursive method; Decidability; Transmission protocol; Cryptography; Tree automaton; Rewriting systems; Rewriting; Equality test; Model driven architecture; Modeling; Undecidability</ED>
<SD>Simultaneidad informatica; Sistema repartido; Método recursivo; Decidibilidad; Protocolo transmisión; Criptografía; Autómata árbol; Reescritura; Test igualdad; Arquitectura basada modelo; Modelización; Indecidibilidad</SD>
<LO>INIST-16343.354000124408310150</LO>
<ID>05-0410073</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 000516 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000516 | 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:05-0410073
   |texte=   Selecting theories and recursive protocols
}}

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

Selecting theories and recursive protocols

Selecting theories and recursive protocols

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