InforLorV4, Main, Merge, bibRecord, 009960

The Rho cube

Identifieur interne : 009960 ( Main/Merge ); précédent : 009959; suivant : 009961

The Rho cube

Auteurs : Horatiu Cirstea [France] ; Claude Kirchner [France] ; Luigi Liquori [France]

Source :

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

RBID : Pascal:01-0247665

Descripteurs français

Pascal (Inist)
- Non déterminisme, Lambda calcul, Réécriture, Syntaxe, Théorie type, Sémantique opérationnelle, Calcul Rho.

English descriptors

KwdEn :
- Lambda calculus, Non determinism, Operational semantics, Rewriting, Syntax, Type theory.

Abstract

The rewriting calculus, or Rho Calculus (pCal), is a simple calculus that uniformly integrates abstraction on patterns and non-determinism. Therefore, it fully integrates rewriting and A-calculus. The original presentation of the calculus was untyped. In this paper we present a uniform way to decorate the terms of the calculus with types. This gives raise to a new presentation à la Church, together with nine (8+1) type systems which can be placed in a p-cube that extends the A-cube of Barendregt. Due to the matching capabilities of the calculus, the type systems use only one abstraction mechanism and therefore gives an original answer to the identification of the standard "λ" and "========Pi;" ors. As a consequence, this brings matching and rewriting as the first class concepts of the Rho-versions of the Logical Framework (LF) of Harper-Honsell-Plotkin, and of the Calculus of Constructions (CC) of Coquand-Huet.

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000960
to stream PascalFrancis, to step Curation: 000116
to stream PascalFrancis, to step Checkpoint: 000877

Links to Exploration step

Pascal:01-0247665

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">The Rho cube</title>
<author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA INRIA INPL ENSMN, BP 23954506</s1>
<s2>Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA INRIA INPL ENSMN, BP 23954506</s1>
<s2>Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA INRIA INPL ENSMN, BP 23954506</s1>
<s2>Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">01-0247665</idno>
<date when="2001">2001</date>
<idno type="stanalyst">PASCAL 01-0247665 INIST</idno>
<idno type="RBID">Pascal:01-0247665</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000960</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000116</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000877</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000877</idno>
<idno type="wicri:doubleKey">0302-9743:2001:Cirstea H:the:rho:cube</idno>
<idno type="wicri:Area/Main/Merge">009960</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">The Rho cube</title>
<author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA INRIA INPL ENSMN, BP 23954506</s1>
<s2>Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA INRIA INPL ENSMN, BP 23954506</s1>
<s2>Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA INRIA INPL ENSMN, BP 23954506</s1>
<s2>Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
</affiliation>
</author>
</analytic>
<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>
</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>Lambda calculus</term>
<term>Non determinism</term>
<term>Operational semantics</term>
<term>Rewriting</term>
<term>Syntax</term>
<term>Type theory</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Non déterminisme</term>
<term>Lambda calcul</term>
<term>Réécriture</term>
<term>Syntaxe</term>
<term>Théorie type</term>
<term>Sémantique opérationnelle</term>
<term>Calcul Rho</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The rewriting calculus, or Rho Calculus (pCal), is a simple calculus that uniformly integrates abstraction on patterns and non-determinism. Therefore, it fully integrates rewriting and A-calculus. The original presentation of the calculus was untyped. In this paper we present a uniform way to decorate the terms of the calculus with types. This gives raise to a new presentation à la Church, together with nine (8+1) type systems which can be placed in a p-cube that extends the A-cube of Barendregt. Due to the matching capabilities of the calculus, the type systems use only one abstraction mechanism and therefore gives an original answer to the identification of the standard "λ" and "========Pi;" ors. As a consequence, this brings matching and rewriting as the first class concepts of the Rho-versions of the Logical Framework (LF) of Harper-Honsell-Plotkin, and of the Calculus of Constructions (CC) of Coquand-Huet.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Nancy</li>
<li>Vandœuvre-lès-Nancy</li>
</settlement>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name>
</region>
<name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name>
<name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge

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

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 009960 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Merge
   |type=    RBID
   |clé=     Pascal:01-0247665
   |texte=   The Rho cube
}}

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

The Rho cube

The Rho cube

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

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