Imperative object-based calculi in co-inductive type theories
Identifieur interne :
000696 ( PascalFrancis/Corpus );
précédent :
000695;
suivant :
000697
Imperative object-based calculi in co-inductive type theories
Auteurs : Alberto Ciaffaglione ;
Luigi Liquori ;
Marino MiculanSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2003.
RBID : Pascal:04-0201758
Descripteurs français
English descriptors
Abstract
We discuss the formalization of Abadi and Cardelli's impC, a paradigmatic object-based calculus with types and side effects, in Co-Inductive Type Theories, such as the Calculus of (Co)Inauctive Constructions (CC(Co)Ind). Instead of representing directly the original system "as it is", we reformulate its syntax and semantics bearing in mind the proof-theoretical features provided by the target metalanguage. On one hand, this methodology allows for a smoother implementation and treatment of the calculus in the metalanguage. On the other, it is possible to see the calculus from a new perspective, thus having the occasion to suggest original and cleaner presentations. We give hence a new presentation of impζ, exploiting natural deduction semantics, (weak) higher-order abstract syntax, and, for a significant fragment of the calculus, coinductive typing systems. This presentation is easier to use and implement than the original one, and the proofs of key metaproperties, e.g. subject reduction, are much simpler. Although all proof developments have been carried out in the Coq system, the solutions we have devised in the encoding of and metareasoning on impζ can be applied to other imperative calculi and proof environments with similar features.
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 2850 |
|---|
| A08 | 01 | 1 | ENG | @1 Imperative object-based calculi in co-inductive type theories |
|---|
| A09 | 01 | 1 | ENG | @1 LPAR 2003 : logic for programming artificial intelligence, and reasoning : Almaty, 22-26 September 2003 |
|---|
| A11 | 01 | 1 | | @1 CIAFFAGLIONE (Alberto) |
|---|
| A11 | 02 | 1 | | @1 LIQUORI (Luigi) |
|---|
| A11 | 03 | 1 | | @1 MICULAN (Marino) |
|---|
| A12 | 01 | 1 | | @1 VARDI (Moshe Y.) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 VORONKOV (Andrei) @9 ed. |
|---|
| A14 | 01 | | | @1 DiMI, University di Udine @3 ITA @Z 1 aut. @Z 3 aut. |
|---|
| A14 | 02 | | | @1 INRIA-LORIA @2 Nancy @3 FRA @Z 2 aut. |
|---|
| A20 | | | | @1 59-77 |
|---|
| A21 | | | | @1 2003 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-20101-7 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000117770190040 |
|---|
| A44 | | | | @0 0000 @1 © 2004 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 29 ref. |
|---|
| A47 | 01 | 1 | | @0 04-0201758 |
|---|
| 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 discuss the formalization of Abadi and Cardelli's impC, a paradigmatic object-based calculus with types and side effects, in Co-Inductive Type Theories, such as the Calculus of (Co)Inauctive Constructions (CC(Co)Ind). Instead of representing directly the original system "as it is", we reformulate its syntax and semantics bearing in mind the proof-theoretical features provided by the target metalanguage. On one hand, this methodology allows for a smoother implementation and treatment of the calculus in the metalanguage. On the other, it is possible to see the calculus from a new perspective, thus having the occasion to suggest original and cleaner presentations. We give hence a new presentation of impζ, exploiting natural deduction semantics, (weak) higher-order abstract syntax, and, for a significant fragment of the calculus, coinductive typing systems. This presentation is easier to use and implement than the original one, and the proofs of key metaproperties, e.g. subject reduction, are much simpler. Although all proof developments have been carried out in the Coq system, the solutions we have devised in the encoding of and metareasoning on impζ can be applied to other imperative calculi and proof environments with similar features. |
|---|
| C02 | 01 | X | | @0 001D02B01 |
|---|
| C02 | 02 | X | | @0 001D02A04 |
|---|
| C02 | 03 | X | | @0 001D02C02 |
|---|
| C03 | 01 | X | FRE | @0 Programmation logique @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Logical programming @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Programación lógica @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Orienté objet @5 02 |
|---|
| C03 | 02 | X | ENG | @0 Object oriented @5 02 |
|---|
| C03 | 02 | X | SPA | @0 Orientado objeto @5 02 |
|---|
| C03 | 03 | 3 | FRE | @0 Théorie type @5 03 |
|---|
| C03 | 03 | 3 | ENG | @0 Type theory @5 03 |
|---|
| C03 | 04 | X | FRE | @0 Métalangage @5 04 |
|---|
| C03 | 04 | X | ENG | @0 Metalanguage @5 04 |
|---|
| C03 | 04 | X | SPA | @0 Metalenguaje @5 04 |
|---|
| C03 | 05 | X | FRE | @0 Typage @5 05 |
|---|
| C03 | 05 | X | ENG | @0 Typing @5 05 |
|---|
| C03 | 05 | X | SPA | @0 Tipificación @5 05 |
|---|
| C03 | 06 | X | FRE | @0 Effet inducteur @5 11 |
|---|
| C03 | 06 | X | ENG | @0 Inductive effect @5 11 |
|---|
| C03 | 06 | X | SPA | @0 Efecto inductor @5 11 |
|---|
| C03 | 07 | X | FRE | @0 Calcul construction @5 12 |
|---|
| C03 | 07 | X | ENG | @0 Structural design @5 12 |
|---|
| C03 | 07 | X | SPA | @0 Cálculo construcción @5 12 |
|---|
| C03 | 08 | X | FRE | @0 Sémantique @5 13 |
|---|
| C03 | 08 | X | ENG | @0 Semantics @5 13 |
|---|
| C03 | 08 | X | SPA | @0 Semántica @5 13 |
|---|
| C03 | 09 | X | FRE | @0 Implémentation @5 16 |
|---|
| C03 | 09 | X | ENG | @0 Implementation @5 16 |
|---|
| C03 | 09 | X | SPA | @0 Implementación @5 16 |
|---|
| C03 | 10 | X | FRE | @0 Déduction @5 17 |
|---|
| C03 | 10 | X | ENG | @0 Deduction @5 17 |
|---|
| C03 | 10 | X | SPA | @0 Deducción @5 17 |
|---|
| N21 | | | | @1 138 |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 Logic for programming, artificial intelligence and reasoning. International conference @2 10 @3 Almaty KAZ @4 2003-09-22 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 04-0201758 INIST |
|---|
| ET : | Imperative object-based calculi in co-inductive type theories |
|---|
| AU : | CIAFFAGLIONE (Alberto); LIQUORI (Luigi); MICULAN (Marino); VARDI (Moshe Y.); VORONKOV (Andrei) |
|---|
| AF : | DiMI, University di Udine/Italie (1 aut., 3 aut.); INRIA-LORIA/Nancy/France (2 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2003; Vol. 2850; Pp. 59-77; Bibl. 29 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | We discuss the formalization of Abadi and Cardelli's impC, a paradigmatic object-based calculus with types and side effects, in Co-Inductive Type Theories, such as the Calculus of (Co)Inauctive Constructions (CC(Co)Ind). Instead of representing directly the original system "as it is", we reformulate its syntax and semantics bearing in mind the proof-theoretical features provided by the target metalanguage. On one hand, this methodology allows for a smoother implementation and treatment of the calculus in the metalanguage. On the other, it is possible to see the calculus from a new perspective, thus having the occasion to suggest original and cleaner presentations. We give hence a new presentation of impζ, exploiting natural deduction semantics, (weak) higher-order abstract syntax, and, for a significant fragment of the calculus, coinductive typing systems. This presentation is easier to use and implement than the original one, and the proofs of key metaproperties, e.g. subject reduction, are much simpler. Although all proof developments have been carried out in the Coq system, the solutions we have devised in the encoding of and metareasoning on impζ can be applied to other imperative calculi and proof environments with similar features. |
|---|
| CC : | 001D02B01; 001D02A04; 001D02C02 |
|---|
| FD : | Programmation logique; Orienté objet; Théorie type; Métalangage; Typage; Effet inducteur; Calcul construction; Sémantique; Implémentation; Déduction |
|---|
| ED : | Logical programming; Object oriented; Type theory; Metalanguage; Typing; Inductive effect; Structural design; Semantics; Implementation; Deduction |
|---|
| SD : | Programación lógica; Orientado objeto; Metalenguaje; Tipificación; Efecto inductor; Cálculo construcción; Semántica; Implementación; Deducción |
|---|
| LO : | INIST-16343.354000117770190040 |
|---|
| ID : | 04-0201758 |
|---|
Links to Exploration step
Pascal:04-0201758
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Imperative object-based calculi in co-inductive type theories</title>
<author><name sortKey="Ciaffaglione, Alberto" sort="Ciaffaglione, Alberto" uniqKey="Ciaffaglione A" first="Alberto" last="Ciaffaglione">Alberto Ciaffaglione</name>
<affiliation><inist:fA14 i1="01"><s1>DiMI, University di Udine</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><author><name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name>
<affiliation><inist:fA14 i1="02"><s1>INRIA-LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Miculan, Marino" sort="Miculan, Marino" uniqKey="Miculan M" first="Marino" last="Miculan">Marino Miculan</name>
<affiliation><inist:fA14 i1="01"><s1>DiMI, University di Udine</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">04-0201758</idno>
<date when="2003">2003</date>
<idno type="stanalyst">PASCAL 04-0201758 INIST</idno>
<idno type="RBID">Pascal:04-0201758</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000696</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Imperative object-based calculi in co-inductive type theories</title>
<author><name sortKey="Ciaffaglione, Alberto" sort="Ciaffaglione, Alberto" uniqKey="Ciaffaglione A" first="Alberto" last="Ciaffaglione">Alberto Ciaffaglione</name>
<affiliation><inist:fA14 i1="01"><s1>DiMI, University di Udine</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><author><name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name>
<affiliation><inist:fA14 i1="02"><s1>INRIA-LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Miculan, Marino" sort="Miculan, Marino" uniqKey="Miculan M" first="Marino" last="Miculan">Marino Miculan</name>
<affiliation><inist:fA14 i1="01"><s1>DiMI, University di Udine</s1>
<s3>ITA</s3>
<sZ>1 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="2003">2003</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>Deduction</term>
<term>Implementation</term>
<term>Inductive effect</term>
<term>Logical programming</term>
<term>Metalanguage</term>
<term>Object oriented</term>
<term>Semantics</term>
<term>Structural design</term>
<term>Type theory</term>
<term>Typing</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Programmation logique</term>
<term>Orienté objet</term>
<term>Théorie type</term>
<term>Métalangage</term>
<term>Typage</term>
<term>Effet inducteur</term>
<term>Calcul construction</term>
<term>Sémantique</term>
<term>Implémentation</term>
<term>Déduction</term>
</keywords><front><div type="abstract" xml:lang="en">We discuss the formalization of Abadi and Cardelli's impC, a paradigmatic object-based calculus with types and side effects, in Co-Inductive Type Theories, such as the Calculus of (Co)Inauctive Constructions (CC<sup>(Co)Ind)</sup>
. Instead of representing directly the original system "as it is", we reformulate its syntax and semantics bearing in mind the proof-theoretical features provided by the target metalanguage. On one hand, this methodology allows for a smoother implementation and treatment of the calculus in the metalanguage. On the other, it is possible to see the calculus from a new perspective, thus having the occasion to suggest original and cleaner presentations. We give hence a new presentation of impζ, exploiting natural deduction semantics, (weak) higher-order abstract syntax, and, for a significant fragment of the calculus, coinductive typing systems. This presentation is easier to use and implement than the original one, and the proofs of key metaproperties, e.g. subject reduction, are much simpler. Although all proof developments have been carried out in the Coq system, the solutions we have devised in the encoding of and metareasoning on impζ can be applied to other imperative calculi and proof environments with similar features.</div><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>2850</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Imperative object-based calculi in co-inductive type theories</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>LPAR 2003 : logic for programming artificial intelligence, and reasoning : Almaty, 22-26 September 2003</s1>
</fA09><fA11 i1="01" i2="1"><s1>CIAFFAGLIONE (Alberto)</s1>
</fA11><fA11 i1="02" i2="1"><s1>LIQUORI (Luigi)</s1>
</fA11><fA11 i1="03" i2="1"><s1>MICULAN (Marino)</s1>
</fA11><fA12 i1="01" i2="1"><s1>VARDI (Moshe Y.)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>VORONKOV (Andrei)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>DiMI, University di Udine</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>3 aut.</sZ>
</fA14><fA14 i1="02"><s1>INRIA-LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</fA14><fA20><s1>59-77</s1>
</fA20><fA21><s1>2003</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-20101-7</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000117770190040</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2004 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>29 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>04-0201758</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 discuss the formalization of Abadi and Cardelli's impC, a paradigmatic object-based calculus with types and side effects, in Co-Inductive Type Theories, such as the Calculus of (Co)Inauctive Constructions (CC<sup>(Co)Ind)</sup>
. Instead of representing directly the original system "as it is", we reformulate its syntax and semantics bearing in mind the proof-theoretical features provided by the target metalanguage. On one hand, this methodology allows for a smoother implementation and treatment of the calculus in the metalanguage. On the other, it is possible to see the calculus from a new perspective, thus having the occasion to suggest original and cleaner presentations. We give hence a new presentation of impζ, exploiting natural deduction semantics, (weak) higher-order abstract syntax, and, for a significant fragment of the calculus, coinductive typing systems. This presentation is easier to use and implement than the original one, and the proofs of key metaproperties, e.g. subject reduction, are much simpler. Although all proof developments have been carried out in the Coq system, the solutions we have devised in the encoding of and metareasoning on impζ can be applied to other imperative calculi and proof environments with similar features.</s0><fC02 i1="01" i2="X"><s0>001D02B01</s0>
</fC02><fC02 i1="02" i2="X"><s0>001D02A04</s0>
</fC02><fC02 i1="03" i2="X"><s0>001D02C02</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Programmation logique</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Logical programming</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Programación lógica</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Orienté objet</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Object oriented</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Orientado objeto</s0>
<s5>02</s5>
</fC03><fC03 i1="03" i2="3" l="FRE"><s0>Théorie type</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="3" l="ENG"><s0>Type theory</s0>
<s5>03</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Métalangage</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Metalanguage</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Metalenguaje</s0>
<s5>04</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Typage</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Typing</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Tipificación</s0>
<s5>05</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Effet inducteur</s0>
<s5>11</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Inductive effect</s0>
<s5>11</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Efecto inductor</s0>
<s5>11</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Calcul construction</s0>
<s5>12</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Structural design</s0>
<s5>12</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Cálculo construcción</s0>
<s5>12</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Sémantique</s0>
<s5>13</s5>
</fC03><fC03 i1="08" i2="X" l="ENG"><s0>Semantics</s0>
<s5>13</s5>
</fC03><fC03 i1="08" i2="X" l="SPA"><s0>Semántica</s0>
<s5>13</s5>
</fC03><fC03 i1="09" i2="X" l="FRE"><s0>Implémentation</s0>
<s5>16</s5>
</fC03><fC03 i1="09" i2="X" l="ENG"><s0>Implementation</s0>
<s5>16</s5>
</fC03><fC03 i1="09" i2="X" l="SPA"><s0>Implementación</s0>
<s5>16</s5>
</fC03><fC03 i1="10" i2="X" l="FRE"><s0>Déduction</s0>
<s5>17</s5>
</fC03><fC03 i1="10" i2="X" l="ENG"><s0>Deduction</s0>
<s5>17</s5>
</fC03><fC03 i1="10" i2="X" l="SPA"><s0>Deducción</s0>
<s5>17</s5>
</fC03><fN21><s1>138</s1>
</fN21><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>Logic for programming, artificial intelligence and reasoning. International conference</s1>
<s2>10</s2>
<s3>Almaty KAZ</s3>
<s4>2003-09-22</s4>
</fA30><server><NO>PASCAL 04-0201758 INIST</NO>
<ET>Imperative object-based calculi in co-inductive type theories</ET>
<AU>CIAFFAGLIONE (Alberto); LIQUORI (Luigi); MICULAN (Marino); VARDI (Moshe Y.); VORONKOV (Andrei)</AU>
<AF>DiMI, University di Udine/Italie (1 aut., 3 aut.); INRIA-LORIA/Nancy/France (2 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2003; Vol. 2850; Pp. 59-77; Bibl. 29 ref.</SO>
<LA>Anglais</LA>
<EA>We discuss the formalization of Abadi and Cardelli's impC, a paradigmatic object-based calculus with types and side effects, in Co-Inductive Type Theories, such as the Calculus of (Co)Inauctive Constructions (CC<sup>(Co)Ind)</sup>
. Instead of representing directly the original system "as it is", we reformulate its syntax and semantics bearing in mind the proof-theoretical features provided by the target metalanguage. On one hand, this methodology allows for a smoother implementation and treatment of the calculus in the metalanguage. On the other, it is possible to see the calculus from a new perspective, thus having the occasion to suggest original and cleaner presentations. We give hence a new presentation of impζ, exploiting natural deduction semantics, (weak) higher-order abstract syntax, and, for a significant fragment of the calculus, coinductive typing systems. This presentation is easier to use and implement than the original one, and the proofs of key metaproperties, e.g. subject reduction, are much simpler. Although all proof developments have been carried out in the Coq system, the solutions we have devised in the encoding of and metareasoning on impζ can be applied to other imperative calculi and proof environments with similar features.</EA><CC>001D02B01; 001D02A04; 001D02C02</CC>
<FD>Programmation logique; Orienté objet; Théorie type; Métalangage; Typage; Effet inducteur; Calcul construction; Sémantique; Implémentation; Déduction</FD>
<ED>Logical programming; Object oriented; Type theory; Metalanguage; Typing; Inductive effect; Structural design; Semantics; Implementation; Deduction</ED>
<SD>Programación lógica; Orientado objeto; Metalenguaje; Tipificación; Efecto inductor; Cálculo construcción; Semántica; Implementación; Deducción</SD>
<LO>INIST-16343.354000117770190040</LO>
<ID>04-0201758</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 000696 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000696 | 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:04-0201758
|texte= Imperative object-based calculi in co-inductive type theories
}}
| 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 |  |
