Rewriting calculus with fixpoints: Untyped and first-order systems
Identifieur interne :
000644 ( PascalFrancis/Corpus );
précédent :
000643;
suivant :
000645
Rewriting calculus with fixpoints: Untyped and first-order systems
Auteurs : Horatiu Cirstea ;
Luigi Liquori ;
Benjamin WackSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2004.
RBID : Pascal:04-0421831
Descripteurs français
- Pascal (Inist)
- Preuve programme,
Lambda calcul,
Concordance forme,
Théorie type,
Orienté objet,
Système réécriture,
Point fixe,
Réécriture,
Abstraction,
Rho calcul,
Langage typé.
English descriptors
- KwdEn :
- Abstraction,
Fix point,
Lambda calculus,
Object oriented,
Pattern matching,
Program proof,
Rewriting,
Rewriting systems,
Rho calculus,
Type theory,
Typed language.
Abstract
The rewriting calculus, also called rho-calculus, is a framework embedding Lambda-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the Lambda-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the Lambda-calculus can be generalized to the rho-calculus: in this paper, we study extensively a first-order rho-calculus à la Church, called ρstk. The type system of ρ→stk allows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting-based language.
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 3085 |
|---|
| A08 | 01 | 1 | ENG | @1 Rewriting calculus with fixpoints: Untyped and first-order systems |
|---|
| A09 | 01 | 1 | ENG | @1 TYPES 2003 : types for proofs and programs : Torino, 30 April - 4 May 2003, revised selected papers |
|---|
| A11 | 01 | 1 | | @1 CIRSTEA (Horatiu) |
|---|
| A11 | 02 | 1 | | @1 LIQUORI (Luigi) |
|---|
| A11 | 03 | 1 | | @1 WACK (Benjamin) |
|---|
| A12 | 01 | 1 | | @1 BERARDI (Stefano) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 COPPO (Mario) @9 ed. |
|---|
| A12 | 03 | 1 | | @1 DAMIANI (Ferruccio) @9 ed. |
|---|
| A14 | 01 | | | @1 LORIA & NANCY II & INRIA & NANCY I, BP 239 @2 54506 Vandoeuvre-lès-Nancy @3 FRA @Z 1 aut. @Z 2 aut. @Z 3 aut. |
|---|
| A20 | | | | @1 147-161 |
|---|
| A21 | | | | @1 2004 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-22164-6 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000117899640100 |
|---|
| A44 | | | | @0 0000 @1 © 2004 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 17 ref. |
|---|
| A47 | 01 | 1 | | @0 04-0421831 |
|---|
| 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 The rewriting calculus, also called rho-calculus, is a framework embedding Lambda-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the Lambda-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the Lambda-calculus can be generalized to the rho-calculus: in this paper, we study extensively a first-order rho-calculus à la Church, called ρstk. The type system of ρ→stk allows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting-based language. |
|---|
| C02 | 01 | X | | @0 001D02A04 |
|---|
| C03 | 01 | X | FRE | @0 Preuve programme @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Program proof @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Prueba programa @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Lambda calcul @5 06 |
|---|
| C03 | 02 | X | ENG | @0 Lambda calculus @5 06 |
|---|
| C03 | 02 | X | SPA | @0 Lambda cálculo @5 06 |
|---|
| C03 | 03 | X | FRE | @0 Concordance forme @5 07 |
|---|
| C03 | 03 | X | ENG | @0 Pattern matching @5 07 |
|---|
| C03 | 04 | 3 | FRE | @0 Théorie type @5 08 |
|---|
| C03 | 04 | 3 | ENG | @0 Type theory @5 08 |
|---|
| C03 | 05 | X | FRE | @0 Orienté objet @5 09 |
|---|
| C03 | 05 | X | ENG | @0 Object oriented @5 09 |
|---|
| C03 | 05 | X | SPA | @0 Orientado objeto @5 09 |
|---|
| C03 | 06 | 3 | FRE | @0 Système réécriture @5 10 |
|---|
| C03 | 06 | 3 | ENG | @0 Rewriting systems @5 10 |
|---|
| C03 | 07 | X | FRE | @0 Point fixe @5 18 |
|---|
| C03 | 07 | X | ENG | @0 Fix point @5 18 |
|---|
| C03 | 07 | X | SPA | @0 Punto fijo @5 18 |
|---|
| C03 | 08 | X | FRE | @0 Réécriture @5 19 |
|---|
| C03 | 08 | X | ENG | @0 Rewriting @5 19 |
|---|
| C03 | 08 | X | SPA | @0 Reescritura @5 19 |
|---|
| C03 | 09 | X | FRE | @0 Abstraction @5 20 |
|---|
| C03 | 09 | X | ENG | @0 Abstraction @5 20 |
|---|
| C03 | 09 | X | SPA | @0 Abstracción @5 20 |
|---|
| C03 | 10 | X | FRE | @0 Rho calcul @4 CD @5 96 |
|---|
| C03 | 10 | X | ENG | @0 Rho calculus @4 CD @5 96 |
|---|
| C03 | 10 | X | SPA | @0 Rho cálculo @4 CD @5 96 |
|---|
| C03 | 11 | X | FRE | @0 Langage typé @4 CD @5 97 |
|---|
| C03 | 11 | X | ENG | @0 Typed language @4 CD @5 97 |
|---|
| C03 | 11 | X | SPA | @0 Lenguaje tipado @4 CD @5 97 |
|---|
| N21 | | | | @1 236 |
|---|
| N44 | 01 | | | @1 OTO |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International workshop on types for proofs and programs @3 Torino ITA @4 2003-04-30 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 04-0421831 INIST |
|---|
| ET : | Rewriting calculus with fixpoints: Untyped and first-order systems |
|---|
| AU : | CIRSTEA (Horatiu); LIQUORI (Luigi); WACK (Benjamin); BERARDI (Stefano); COPPO (Mario); DAMIANI (Ferruccio) |
|---|
| AF : | LORIA & NANCY II & INRIA & NANCY I, BP 239/54506 Vandoeuvre-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. 2004; Vol. 3085; Pp. 147-161; Bibl. 17 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | The rewriting calculus, also called rho-calculus, is a framework embedding Lambda-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the Lambda-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the Lambda-calculus can be generalized to the rho-calculus: in this paper, we study extensively a first-order rho-calculus à la Church, called ρstk. The type system of ρ→stk allows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting-based language. |
|---|
| CC : | 001D02A04 |
|---|
| FD : | Preuve programme; Lambda calcul; Concordance forme; Théorie type; Orienté objet; Système réécriture; Point fixe; Réécriture; Abstraction; Rho calcul; Langage typé |
|---|
| ED : | Program proof; Lambda calculus; Pattern matching; Type theory; Object oriented; Rewriting systems; Fix point; Rewriting; Abstraction; Rho calculus; Typed language |
|---|
| SD : | Prueba programa; Lambda cálculo; Orientado objeto; Punto fijo; Reescritura; Abstracción; Rho cálculo; Lenguaje tipado |
|---|
| LO : | INIST-16343.354000117899640100 |
|---|
| ID : | 04-0421831 |
|---|
Links to Exploration step
Pascal:04-0421831
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Rewriting calculus with fixpoints: Untyped and first-order systems</title>
<author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA & NANCY II & INRIA & NANCY I, BP 239</s1>
<s2>54506 Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 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="01"><s1>LORIA & NANCY II & INRIA & NANCY I, BP 239</s1>
<s2>54506 Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><author><name sortKey="Wack, Benjamin" sort="Wack, Benjamin" uniqKey="Wack B" first="Benjamin" last="Wack">Benjamin Wack</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA & NANCY II & INRIA & NANCY I, BP 239</s1>
<s2>54506 Vandoeuvre-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">04-0421831</idno>
<date when="2004">2004</date>
<idno type="stanalyst">PASCAL 04-0421831 INIST</idno>
<idno type="RBID">Pascal:04-0421831</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000644</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Rewriting calculus with fixpoints: Untyped and first-order systems</title>
<author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA & NANCY II & INRIA & NANCY I, BP 239</s1>
<s2>54506 Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 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="01"><s1>LORIA & NANCY II & INRIA & NANCY I, BP 239</s1>
<s2>54506 Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><author><name sortKey="Wack, Benjamin" sort="Wack, Benjamin" uniqKey="Wack B" first="Benjamin" last="Wack">Benjamin Wack</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA & NANCY II & INRIA & NANCY I, BP 239</s1>
<s2>54506 Vandoeuvre-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="2004">2004</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>Abstraction</term>
<term>Fix point</term>
<term>Lambda calculus</term>
<term>Object oriented</term>
<term>Pattern matching</term>
<term>Program proof</term>
<term>Rewriting</term>
<term>Rewriting systems</term>
<term>Rho calculus</term>
<term>Type theory</term>
<term>Typed language</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Preuve programme</term>
<term>Lambda calcul</term>
<term>Concordance forme</term>
<term>Théorie type</term>
<term>Orienté objet</term>
<term>Système réécriture</term>
<term>Point fixe</term>
<term>Réécriture</term>
<term>Abstraction</term>
<term>Rho calcul</term>
<term>Langage typé</term>
</keywords><front><div type="abstract" xml:lang="en">The rewriting calculus, also called rho-calculus, is a framework embedding Lambda-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the Lambda-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the Lambda-calculus can be generalized to the rho-calculus: in this paper, we study extensively a first-order rho-calculus à la Church, called ρ<sup>stk</sup>
. The type system of ρ<sub>→</sub>
<sup>stk</sup>
allows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting-based language.</div><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>3085</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Rewriting calculus with fixpoints: Untyped and first-order systems</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>TYPES 2003 : types for proofs and programs : Torino, 30 April - 4 May 2003, revised selected papers</s1>
</fA09><fA11 i1="01" i2="1"><s1>CIRSTEA (Horatiu)</s1>
</fA11><fA11 i1="02" i2="1"><s1>LIQUORI (Luigi)</s1>
</fA11><fA11 i1="03" i2="1"><s1>WACK (Benjamin)</s1>
</fA11><fA12 i1="01" i2="1"><s1>BERARDI (Stefano)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>COPPO (Mario)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="03" i2="1"><s1>DAMIANI (Ferruccio)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>LORIA & NANCY II & INRIA & NANCY I, BP 239</s1>
<s2>54506 Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</fA14><fA20><s1>147-161</s1>
</fA20><fA21><s1>2004</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-22164-6</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000117899640100</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2004 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>17 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>04-0421831</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>The rewriting calculus, also called rho-calculus, is a framework embedding Lambda-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the Lambda-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the Lambda-calculus can be generalized to the rho-calculus: in this paper, we study extensively a first-order rho-calculus à la Church, called ρ<sup>stk</sup>
. The type system of ρ<sub>→</sub>
<sup>stk</sup>
allows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting-based language.</s0><fC02 i1="01" i2="X"><s0>001D02A04</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Preuve programme</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Program proof</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Prueba programa</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Lambda calcul</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Lambda calculus</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Lambda cálculo</s0>
<s5>06</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Concordance forme</s0>
<s5>07</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Pattern matching</s0>
<s5>07</s5>
</fC03><fC03 i1="04" i2="3" l="FRE"><s0>Théorie type</s0>
<s5>08</s5>
</fC03><fC03 i1="04" i2="3" l="ENG"><s0>Type theory</s0>
<s5>08</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Orienté objet</s0>
<s5>09</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Object oriented</s0>
<s5>09</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Orientado objeto</s0>
<s5>09</s5>
</fC03><fC03 i1="06" i2="3" l="FRE"><s0>Système réécriture</s0>
<s5>10</s5>
</fC03><fC03 i1="06" i2="3" l="ENG"><s0>Rewriting systems</s0>
<s5>10</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Point fixe</s0>
<s5>18</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Fix point</s0>
<s5>18</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Punto fijo</s0>
<s5>18</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Réécriture</s0>
<s5>19</s5>
</fC03><fC03 i1="08" i2="X" l="ENG"><s0>Rewriting</s0>
<s5>19</s5>
</fC03><fC03 i1="08" i2="X" l="SPA"><s0>Reescritura</s0>
<s5>19</s5>
</fC03><fC03 i1="09" i2="X" l="FRE"><s0>Abstraction</s0>
<s5>20</s5>
</fC03><fC03 i1="09" i2="X" l="ENG"><s0>Abstraction</s0>
<s5>20</s5>
</fC03><fC03 i1="09" i2="X" l="SPA"><s0>Abstracción</s0>
<s5>20</s5>
</fC03><fC03 i1="10" i2="X" l="FRE"><s0>Rho calcul</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="10" i2="X" l="ENG"><s0>Rho calculus</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="10" i2="X" l="SPA"><s0>Rho cálculo</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="11" i2="X" l="FRE"><s0>Langage typé</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03><fC03 i1="11" i2="X" l="ENG"><s0>Typed language</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03><fC03 i1="11" i2="X" l="SPA"><s0>Lenguaje tipado</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03><fN21><s1>236</s1>
</fN21><fN44 i1="01"><s1>OTO</s1>
</fN44><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>International workshop on types for proofs and programs</s1>
<s3>Torino ITA</s3>
<s4>2003-04-30</s4>
</fA30><server><NO>PASCAL 04-0421831 INIST</NO>
<ET>Rewriting calculus with fixpoints: Untyped and first-order systems</ET>
<AU>CIRSTEA (Horatiu); LIQUORI (Luigi); WACK (Benjamin); BERARDI (Stefano); COPPO (Mario); DAMIANI (Ferruccio)</AU>
<AF>LORIA & NANCY II & INRIA & NANCY I, BP 239/54506 Vandoeuvre-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. 2004; Vol. 3085; Pp. 147-161; Bibl. 17 ref.</SO>
<LA>Anglais</LA>
<EA>The rewriting calculus, also called rho-calculus, is a framework embedding Lambda-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of the Lambda-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the Lambda-calculus can be generalized to the rho-calculus: in this paper, we study extensively a first-order rho-calculus à la Church, called ρ<sup>stk</sup>
. The type system of ρ<sub>→</sub>
<sup>stk</sup>
allows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting-based language.</EA><CC>001D02A04</CC>
<FD>Preuve programme; Lambda calcul; Concordance forme; Théorie type; Orienté objet; Système réécriture; Point fixe; Réécriture; Abstraction; Rho calcul; Langage typé</FD>
<ED>Program proof; Lambda calculus; Pattern matching; Type theory; Object oriented; Rewriting systems; Fix point; Rewriting; Abstraction; Rho calculus; Typed language</ED>
<SD>Prueba programa; Lambda cálculo; Orientado objeto; Punto fijo; Reescritura; Abstracción; Rho cálculo; Lenguaje tipado</SD>
<LO>INIST-16343.354000117899640100</LO>
<ID>04-0421831</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 000644 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000644 | 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-0421831
|texte= Rewriting calculus with fixpoints: Untyped and first-order 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 |  |
