A Rho Cube
Identifieur interne : 009E11 ( Main/Merge ); précédent : 009E10; suivant : 009E12A Rho Cube
Auteurs : Horatiu Cirstea ; Claude Kirchner ; Luigi LiquoriSource :
English descriptors
- KwdEn :
Abstract
The rewriting calculus, or Rho Calculus, is a simple calculus that uniformly integrates abstraction on patterns and non-determinism. Therefore, it fully integrates rewriting and lambda-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 a la Church, together with nine (8+1) type systems which can be placed in a RHO-cube that extends the Lambda-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 ``lambda'' and ``pi'' abstractors. 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 Crin, to step Corpus: 002B64
- to stream Crin, to step Curation: 002B64
- to stream Crin, to step Checkpoint: 001779
Links to Exploration step
CRIN:cirstea00dLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" wicri:score="0">A Rho Cube</title></titleStmt><publicationStmt><idno type="RBID">CRIN:cirstea00d</idno><date when="2000" year="2000">2000</date><idno type="wicri:Area/Crin/Corpus">002B64</idno><idno type="wicri:Area/Crin/Curation">002B64</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">002B64</idno><idno type="wicri:Area/Crin/Checkpoint">001779</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">001779</idno><idno type="wicri:Area/Main/Merge">009E11</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr">A Rho Cube</title><author><name sortKey="Cirstea, Horatiu" sort="Cirstea, Horatiu" uniqKey="Cirstea H" first="Horatiu" last="Cirstea">Horatiu Cirstea</name></author><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name></author><author><name sortKey="Liquori, Luigi" sort="Liquori, Luigi" uniqKey="Liquori L" first="Luigi" last="Liquori">Luigi Liquori</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>rewriting</term><term>type systems</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2333">The rewriting calculus, or Rho Calculus, is a simple calculus that uniformly integrates abstraction on patterns and non-determinism. Therefore, it fully integrates rewriting and lambda-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 a la Church, together with nine (8+1) type systems which can be placed in a RHO-cube that extends the Lambda-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 ``lambda'' and ``pi'' abstractors. 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></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 009E11 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 009E11 | 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é= CRIN:cirstea00d
|texte= A Rho Cube
}}
| This area was generated with Dilib version V0.6.33. |  |