# papers.bib

@INPROCEEDINGS{CirsteaKirchnerCCL98,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {$\rho$-calculus. {I}ts {S}yntax and {B}asic {P}roperties},
year = {1998},
pdf = {data/ccl98.pdf},
booktitle = {Workshop CCL'98},
month = SEP
}

@TECHREPORT{CirsteaKirchnerINRIA99,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {An introduction to the rewriting calculus},
institution = {INRIA},
month = DEC,
number = {RR-3818},
type = {Research Report},
year = {1999},
url = {http://www.inria.fr/rrrt/rr-3818.html},
abstract = {The rho-calculus is a new calculus that integrates
in a uniform and simple setting first-order rewriting,
lambda-calculus and non-deterministic computations. This
report describes the calculus from its syntax to its basic
properties in the untyped case. We show how it embeds
first-order conditional rewriting and lambda-calculus. Finally
we use the rho-calculus to give an operational semantics to
the rewrite based language ELAN.}
}

@INCOLLECTION{CirsteaKirchner-LivreFroCoS99,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {Combining Higher-Order and First-Order Computation Using
$\rho$-calculus: Towards a semantics of {{\sf ELAN}}},
booktitle = {Frontiers of Combining Systems 2},
publisher = {Wiley},
year = {1998},
month = OCT,
editor = {Gabbay, Dov and de Rijke, Maarten},
series = {Research Studies, ISBN 0863802524, appeared in 1999},
pages = {95--120},
comment = {Invited presentation by CK}
}

@INPROCEEDINGS{CirsteaKirchner-Asian98,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {The rewriting calculus as a semantics of {{\sf ELAN}}},
booktitle = {{4th Asian Computing Science Conference}},
editor = {Hsiang, J. and Ohori, A.},
year = {1998},
pdf = {data/asian98.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 1538,
month = DEC,
pages = {8--10},
comment = {Invited presentation by CK}
}

@INPROCEEDINGS{CirsteaKirchnerWRLA2000,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {The Typed Rewriting Calculus},
year = {2000},
booktitle = {Third International Workshop on Rewriting Logic and
Application },
month = SEP,
pdf = {data/wrla2000.pdf},
abstract = {The rewriting calculus is a rule construction and
application framework. As such it embeds in a uniform way term
rewriting and lambda-calculus. Since rule application is an
explicit object of the calculus, it allows us also to handle
the set of results explicitly.
We present a simply typed version of the rewriting
calculus. With a good choice of the type system, we show that
the calculus is type preserving and terminating, i.e. verifies
the subject reduction and strong normalization properties.
}
}

@INPROCEEDINGS{CirsteaKirchnerLiquoriMatchingPower-RTA2001,
author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi},
title = {{M}atching {P}ower},
year = {2001},
booktitle = {Proceedings of {RTA'2001}},
publisher = {Springer-Verlag},
series = {{Lecture Notes in Computer Science}},
month = MAY,
ps = {data/rta2001.pdf},
abstract = {In this paper we give a simple and uniform
presentation of the rewriting calculus, also called
rho-calculus.  In addition to its simplicity, this formulation
computations	explicitly allows us to encode complex structures such as
lists, sets, and objects.  We provide extensive examples of
the calculus, and we focus on its ability to represent some
object oriented calculi, namely the Lambda Calculus of Objects
of Fisher, Honsell, and Mitchell, and the Object Calculus of
Abadi and Cardelli. Furthermore, the calculus allows us to get
object oriented constructions unreachable in other calculi. In
summa, we intend to show that because of its matching ability,
the rho-calculus represents a lingua franca'' to naturally
encode many paradigms of computations. This enlightens the
capabilities of the rewriting calculus based language ELAN to
be used as a logical as well as powerful semantical framework.
}
}

@PHDTHESIS{CirsteaThese2000,
author = {Cirstea,~Horatiu},
title = {Calcul de r\'e\'ecriture~: fondements et applications},
school = {Université Henri Poincaré - Nancy I},
year = {2000},
note = {October 25},
pdf = {data/these.pdf},
abstract = {L'objet de cette thèse est l'étude d'un calcul
permettant de décrire l'application de règles de réécriture
conditionnelles et de représenter les résultats obtenus. Nous
introduisons le calcul de réécriture, appelé aussi le
rho-calcul, qui généralise la réécriture du premier ordre et
le lambda-calcul tout en permettant d'exprimer le
non-déterminisme. Dans notre approche, l'opérateur
d'abstraction ainsi que l'opérateur d'application sont des
objets du calcul. Le résultat d'une réduction dans le calcul
de réécriture est soit un ensemble vide représentant l'échec
de l'application, soit un singleton représentant un résultat
déterministe, soit un ensemble ayant plusieurs éléments
représentant un choix non-déterministe de résultats.
Au cours de cette thèse nous nous concentrons sur les
propriétés du calcul de réécriture où le filtrage utilisé pour
lier les variables à leurs valeurs actuelles est
syntaxique. Nous définissons des stratégies d'évaluation
garantissant la confluence du calcul et nous montrons que ces
stratégies deviennent triviales pour des restrictions du
calcul de réécriture général à des calculs plus simples comme
le lambda-calcul. Le calcul de réécriture n'est pas terminant
dans le cas non-typé mais la terminaison forte est obtenue en
introduisant un typage des termes.
Dans le calcul de réécriture étendu par un opérateur
permettant de tester l'échec de l'application nous définissons
des termes représentant la normalisation \textit{innermost} et
\textit{outermost} par rapport à un ensemble de règles de
réécriture. En utilisant ces termes, nous obtenons un codage
naturel et concis de la réécriture conditionnelle. Enfin, à
partir de la représentation des règles de réécriture
conditionnelles, nous montrons comment le calcul de réécriture
peut être employé pour donner une sémantique au langage {\sf ELAN},
un langage basé sur l'application de règles de réécriture
contrôlées par des stratégies.}
}

@INPROCEEDINGS{CirsteaKirchnerLiquoriRhoCube2001,
author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi},
title = {The {R}ho {C}ube},
pages = {166-180},
booktitle = {Foundations of Software Science and Computation Structures,
{http://www.disi.unige.it/etaps2001}{ETAPS'2001}},
editor = {Honsell, Furio},
month = APR,
series = {{http://www.springer.de/comp/lncs/index.html}{Lecture Notes in Computer Science}},
year = {2001},
pdf = {data/fossacs2001.pdf},
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 of Harper-Honsell-Plotkin, and of the Calculus of
Constructions of Coquand-Huet.
}
}

@ARTICLE{rhoCalIGLP-I-2001,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {The rewriting calculus --- {Part~I}},
journal = {Logic Journal of the Interest Group in Pure and
Applied Logics},
year = {2001},
volume = {9},
number = {3},
pages = {427--463},
month = MAY,
pdf = {data/iglp1.pdf},
abstract = {The Rho-calculus integrates in a uniform and
simple setting first-order rewriting, Lambda-calculus and
non-deterministic computations.  Its abstraction mechanism is
based on the rewrite rule formation and its main evaluation
rule is based on matching modulo a theory T.
In this first part, the calculus is motivated and its syntax
and evaluation rules for any theory T are presented.  In the
syntactic case, i.e. when T is the empty theory, we study its
basic properties for the untyped case. We first show how it
uniformly encodes Lambda-calculus as well as first-order
rewriting derivations. Then we provide sufficient conditions
for ensuring the confluence of the calculus.
The rewriting calculus is a rule construction and application
framework. As such it embeds in a uniform way term rewriting
and Lambda-calculus. Since rule application is an explicit
object of the calculus, it allows us also to handle the set of
results explicitly.
We present a simply typed version of the rewriting
calculus. With a good choice of the type system, we show that
the calculus is type preserving and terminating, i.e. verifies
the subject reduction and strong normalization properties.
}
}

@ARTICLE{rhoCalIGLP-II-2001,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {The rewriting calculus --- {Part~II}},
journal = {Logic Journal of the Interest Group in Pure and
Applied Logics},
year = {2001},
volume = {9},
number = {3},
pages = {465--498},
month = MAY,
pdf = {data/iglp2.pdf},
abstract = {The Rho-calculus integrates in a uniform and
simple setting first-order rewriting, Lambda-calculus and
non-deterministic computations.  Its abstraction mechanism is
based on the rewrite rule formation and its main evaluation
rule is based on matching modulo a theory T.
We have seen in the first part of this work the motivations,
definitions and basic properties of the rho-calculus.  This
second part is first devoted to the use of the rho-calculus
for encoding a (conditional) rewrite relation. To this end we
extend the calculus with a first'' operator whose purpose is
to detect rule application failure. This extension allows us
to express recursively rule application and therefore to
encode strategy based rewriting processes. We then use this
extended calculus to give an operational semantics to ELAN
programs.
We conclude with an overview of ongoing and future works on
rho-calculus.
}
}

@ARTICLE{rhoCalIGLP-I+II-2001,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {The rewriting calculus --- {Part~I {\em and} II}},
journal = {Logic Journal of the Interest Group in Pure and Applied Logics},
year = {2001},
volume = {9},
number = {3},
pages = {427--498},
month = MAY
}

@ARTICLE{BKKR-IJFCS-2001,
author = {Borovansky,~Peter and Kirchner,~Claude and Ringeissen,~Christophe and Kirchner,~Helene},
title = {Rewriting with strategies in {{\sf ELAN}}:
a functional semantics},
journal = {{International Journal of Foundations of Computer Science}},
volume = {12},
number = {1},
pages = {69--98},
month = FEB,
year = {2001},
pdf = {data/fuji.pdf},
abstract = {In this work, we consider term rewriting from a
functional point of view.  A rewrite rule is a function that
can be applied to a term using an explicit application
function. From this starting point, we show how to build more
elaborated functions, describing first rewrite derivations,
then sets of derivations.  These functions, that we call
strategies, can themselves be defined by rewrite rules and the
construction can be iterated leading to higher-order
strategies.  Furthermore, the application function is itself
defined using rewriting in the same spirit.  We present this
calculus and study its properties. Its implementation in the
ELAN language is used to motivate and exemplify the whole
approach. The expressiveness of {\sf ELAN} is illustrated by
examples of polymorphic functions and strategies.
}
}

@INPROCEEDINGS{wmp2000,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {Rewriting and Multisets in the Rewriting Calculus and ELAN},
booktitle = {{Workshop on Multiset Processing, Curtea de Arges, Romania}},
year = {2000},
month = { Aug},
pdf = {data/wmp2000.pdf},
abstract = {The rewriting calculus is a new calculus that integrates in a uniform and simple setting first-order rewriting, lambda-calculus and non-deterministic computations. The main design concept of the rewriting calculus is to make all the basic ingredients of rewriting explicit objects, in particular the notions of rule application and multisets of results. This paper describes the calculus from its syntax to its basic properties in the untyped case. The rewriting calculus embeds first-order conditional rewriting and lambda-calculus and it can be used in order to give an operational semantics to the rewrite based language Elan.  We show how the set-like data structures are easily represented in Elan and how this can be used in order to specify protocols.  }
}

@ARTICLE{multisetIST-I-2001,
author = {Cirstea,~Horatiu and Kirchner,~Claude},
title = {{R}ewriting and {M}ultisets in {R}ho-calculus and {{\sf ELAN}}},
journal = {Romanian Journal of Information, Science and Technology},
year = {2001},
volume = {4},
number = {1-2},
pdf = {data/rjist.pdf},
pages = {33--48},
note = {ISSN: 1453-8245}
}

@INPROCEEDINGS{FaureKirchnerRhoException-RTA2002,
author = {Faure,~Germain and Kirchner,~Claude},
title = {Exceptions in the rewriting calculus},
pages = {66--82},
booktitle = {Proceedings of the RTA conference},
volume = {2378},
year = {2002},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
editor = {Tison, Sophie},
month = JUL,
pdf = {data/rhoException.pdf},
abstract = {In the context of the rewriting calculus, we
introduce and study an exception mechanism that allows us to
express in a simple way rewriting strategies and that is
therefore also useful for expressing theorem proving
tactics. The proposed exception mechanism is expressed in a
confluent calculus which gives the ability to simply express
the semantics of the first tactical and to describe in full
details the expression of conditional rewriting.}
}

@TECHREPORT{FaureMIM1-2001,
author = {Faure,~Germain},
title = {Etude des propri\'et\'es du calcul de réécriture:
du rho au rho-epsilon calcul},
institution = {LORIA et ENS Lyon},
type = {Rapport du stage de première année du Magist\ere
d'Informatique et de Mod\'elisation de l'ENS Lyon},
month = SEP,
year = {2001},
ps = {data/rhoGermain.pdf},
abstract = {Abstract {html/rhoGermain-resume.html}{in French}, or
{html/rhoGermain-abstract.html}{in English}}
}

@TECHREPORT{BenjaminDEA2002,
author = {Wack,~Benjamin},
title = {Aspects typés du calcul de réécriture},
institution = {LORIA - ENS Lyon},
year = {2002},
type = {Rapport de DEA},
month = JUL,
pdf = {http://www.loria.fr/~wack/memoireDEA.pdf},
abstract = {
Le calcul de réécriture, ou rho-calcul, intègre dans un même système le
lambda-calcul et la réécriture. Pour cela, les abstractions ne se font
plus seulement sur des variables mais sur des motifs. On profite ainsi à
la fois des mécanismes d'ordre supérieur du lambda-calcul et de
l'expressivité du filtrage de la réécriture. La complexité des divers
éléments du calcul font qu'il n'est pas confluent et donc qu'il faut
définir des stratégies, ou des restrictions, pour assurer la confluence.
Nous nous intéressons ici au rho-calcul en tant qu'extension du
lambda-calcul et nous en étudions les aspects typés. Notre étude se base
sur une généralisation du cube de Barendregt, où les deux abstracteurs
lambda et Pi sont unifiés en un seul. Il nous faut aussi tenir compte
des nouveaux éléments du rho-calcul : puissance du filtrage,
non-déterminisme, problèmes de confluence.
Sous les bonnes conditions, nous parvenons ainsi à prouver la plupart
des propriétés habituelles des calculs typés : lemme de substitution,
correction, préservation du type, consistance. Cependant, l'unicité du
type n'est généralement plus valable, notamment à cause de
l'unification des abstracteurs. Nous décrivons le nombre de
types distincts que peut avoir un terme donné, et nous montrons enfin
que l'unicité du typage reste valide dans les systèmes simplement typé
et polymorphe.
}
}

@INPROCEEDINGS{HOR2002,
author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi and Wack,~Benjamin},
title = {The rewriting calculus : some results, some problems},
booktitle = {The first international workshop on {H}igher-{O}rder
{R}ewriting},
pages = {1 -- 2},
year = {2002},
editor = {Kesner, Delia and van Raamsdonk, Femke and Nipkow, Tobias},
month = JUL,
organization = {FLoC'02},
ps = {http://www.lri.fr/~kesner/hor/proc/proc.ps},
abstract = {
The rewriting calculus, also called rho-calculus, embeds in a same
setting the lambda-calculus and the rewriting, 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. It is worth noticing that the complexity of the calculus
breaks the confluence property, so that we need to define appropriate
strategies, or restrictions, in order to recover it.
We choose here to look at the rho-calculus as an extension of the
lambda-calculus, and we study the typed aspects. Our study is based upon
a generalization of Barendregt's lambda-cube, in which we unify both
abstractors lambda and Pi into a single one. We need to deal with the
original features of the rho-calculus too: matching power,
non-determinism, confluence issues.
With proper restrictions, we have proved most of the usual properties
for typed calculi: substitution lemma, correctness of types, subject
reduction, consistency. However, the uniqueness of typing is no longer
valid mainly because of the unification of both abstractors. We are
able to describe how many distinct types a term can admit and we can
still prove the uniqueness of typing for the two most restrictive
systems: simply typed and polymorphic.
}
}

@TECHREPORT{ClaraDEA2002,
author = {Bertolissi,~Clara},
title = {dea},
institution = {LORIA},
year = {2002},
type = {Rapport de DEA},
month = JUL,
abstract = {Dans ce rapport notre but est d'analyser la
correspondance entre le calcul de réécriture et les relations de
réécriture d'ordre supérieur. En particulier, nous montrons que pour
toute réduction dans un CRS nous avons une réduction correspondante
dans le calcul de réécriture et nous fournissons une traduction
directe des CRS dans le calcul de réécriture.},
ps = {data/deaClara.pdf}
}

@INPROCEEDINGS{RhoCal-Wrla2002,
author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi},
title = {Rewriting Calculus with(out) Types},
booktitle = {Proceedings of the fourth workshop on rewriting logic
and applications},
year = {2002},
editor = {Gadducci, Fabio and Montanari, Ugo},
publisher = {Electronic Notes in Theoretical Computer Science},
month = SEP,
comment = {Invited presentation by LL},
pdf = {data/wrla2002.pdf},
abstract = {The last few years have seen the development of a
new calculus which can be considered as the outcome of the
last decade of various researches on (higher order) term
rewriting systems, and lambda calculi.  In the Rewriting
Calculus (or Rho Calculus), algebraic rules are
considered as sophisticated forms of lambda terms with
patterns'', and rule applications as lambda applications with
pattern matching facilities.

The calculus can be customized'' to work modulo
sophisticated algebraic theories, like commutativity,
associativity, associativity-commutativity, etc.  This allows
us to encode complex structures such as list, sets, and more
generally objects.  The calculus can be either be presented
à la Curry'' or à la Church'' without sacrificing
readability and without complicating too much the metatheory.

The Rewriting Calculus could represent a \textit{lingua
franca} to encode many paradigms of computations together with
a formal basis used to build powerful theorem provers based on
lambda calculus and efficient rewriting, and a step towards
new proof engines based on the Curry-Howard isomorphism.
}
}

@INPROCEEDINGS{ppts-popl2003,
author = {Barthe,~Gilles and Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi},
title = {Pure Patterns Type Systems},
booktitle = {{ Principles of Programming Languages - POPL2003, New Orleans, USA}},
year = 2003,
month = JAN,
publisher = {ACM},
pdf = {data/popl2003.pdf},
abstract = { We introduce a new framework of algebraic pure
type systems in which we consider rewrite rules as lambda
terms with patterns and rewrite rule application as
abstraction application with built-in matching facilities.
This framework, that we call \textit{Pure Pattern Type
Systems''}, is particularly well-suited for the foundations of
programming (meta)languages and proof assistants since it
provides in a fully unified setting higher-order capabilities
and pattern matching ability together with powerful type
systems.  We prove some standard properties like confluence
and subject reduction for the case of a syntactic theory and
under a syntactical restriction over the shape of patterns.
We also conjecture the strong normalization of typable terms.
This work should be seen as a contribution to a formal
connection between logics and rewriting, and a step towards
new proof engines based on the Curry-Howard isomorphism.}
}

@INPROCEEDINGS{rewritingStrategiesWRS2003,
author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi and Wack,~Benjamin},
title = {Rewrite Strategies in the Rewriting Calculus},
booktitle = {{Proceedings of the Third International Workshop on Reduction Strategies
in Rewriting and Programming }},
year = 2003,
month = JUN,
publisher = {Electronic Notes in Theoretical Computer Science},
editor = {Gramlich, Bernhard and Lucas, Salvador},
pdf = {data/wrs2003.pdf},
abstract = { This paper presents an overview on the use of the
rewriting calculus to express rewrite strategies. We motivate
first the use of rewrite strategies by examples in the elan\
language. We then show how this has be modelled in the initial
version of the rewriting calculus and how the matching power
of this framework facilitates the writing of powerful
strategies. }
}

@TECHREPORT{Faure03a,
author = {Faure,~Germain},
title = {Explicit Rewriting Calculus},
year = { 2003},
month = { Sep},
institution = {ENS-Cachan,IRISA,LORIA},
type = {Master Thesis},
abstract = {The contributions of this report are twofold.
First, we will give the intuition  of how  programs can be represented
in the rewriting calculus. We will compare with the lambda-calculus and
take  many examples of OCaml programs.  Secondly,  we  propose,  study
and  exemplify  a  rewriting calculus with explicit constraint handling.
In this calculus, matching and application of   substitutions become
explicit. The approach is really modular, allowing extension to
arbitrary matching theories. We will also prove that the calculus is
powerful enough to deal with errors.  We will afterwards prove the
confluence of the calculus and the termination of the explicit'' part
of the calculus, some non trivial proofs. We conclude by an other
extension of the calculus to handle composition of substitutions. },
ps = {data/reportdeaGF.pdf}
}

@TECHREPORT{CtreExKlop,
author = {Wack, Benjamin},
title = {Klop counter example in the Rho-Calculus},
institution = {LORIA},
year = {2003},
type = {Draft notes},
abstract = {We give a rho-translation of Klop's classical example about non-confluence for higher-order systems with non-linear matching.},
ps = {data/spoofer.pdf}
}

@INPROCEEDINGS{BertolissiCirsteaKirchnerRULE03,
author = {Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
title = {{Translating Combinatory Reduction Systems into the
Rewriting Calculus}},
booktitle = {{Proceedings of the 4th International Workshop on
Rule-Based Programming
Valencia, Spain, June 9, 2003}},
year = 2003,
month = JUN,
publisher = {Electronic Notes in Theoretical Computer Science},
editor = {Giavitto, Jean-Louis and Moreau, Pierre-Etienne},
abstract = {The last few years have seen the development of the
\emph{rewriting calculus} (or rho-calculus, RHO) that extends
first order term rewriting and $\lambda$-calculus. The integration
of these two latter formalisms has been already handled either by
enriching first-order rewriting with higher-order capabilities,
like in the \emph{Combinatory Reduction Systems}, or by adding to
$\lambda$-calculus algebraic features. The different higher-order
rewriting systems and the rewriting calculus share similar
concepts and have similar applications, and thus, it seems natural
to compare these formalisms.  We analyze in this paper the
relationship between the Rewriting Calculus and the Combinatory
Reduction Systems and we present a translation of
CRS-terms and rewrite rules into rho-terms and we show
that for any CRS-reduction we have a corresponding rho-reduction.},
pdf = {data/rule03crsro.pdf}
}

@INPROCEEDINGS{CirsteaLiquoriWackTYPES03,
author = {Cirstea,~Horatiu and Liquori,~Luigi and Wack,~Benjamin},
title = {Rewriting Calculus with Fixpoints: Untyped and First-order Systems},
year = {2003},
volume = {3085},
publisher = {Springer},
pdf = {data/types2003.pdf},
abstract = { The rewriting calculus, also called rho-calculus, is a framework embed
ding 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 \a 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.}
}

@INPROCEEDINGS{CirsteaFaureKirchnerWLRA2004,
author = {Cirstea,~Horatiu and Faure,~Germain and Kirchner,~Claude},
title = {A rho-calculus of explicit constraint application},
booktitle = {Proceedings of the 5th workshop on rewriting logic
and applications},
year = {2004},
publisher = {vol. 117 of Electronic Notes in Theoretical Computer Science},
pdf = {data/wrla2004-19.pdf},
abstract = { Theoretical presentations of the rho-calculus often treat the
matching constraint computations as an atomic operation although
matching constraints are explicitly expressed. Actual implementations
have to take a much more realistic view: computations needed in order
to find the solutions of a matching equation can be really important
in some matching theories and the substitution application usually
involves a term traversal.
Following the works on explicit substitutions in the
\lambda-calculus, we propose, study and exemplify a rho-calculus with explicit constraint handling, up to the level of
substitution applications. The approach is general, allowing the extension
to various matching theories.
We show that the calculus is powerful enough to deal with errors.
We establish the confluence of the calculus and the termination of the
explicit constraint handling and application sub-calculus.}
}

@INPROCEEDINGS{LiquoriWackWLRA2004,
author = {Liquori,~Luigi and Wack,~Benjamin},
title = {The Polymorphic Rewriting-calculus
[Type Checking vs. Type Inference]},
booktitle = {Proceedings of the 5th workshop on rewriting logic
and applications},
year = {2004},
publisher = {vol. 117 of Electronic Notes in Theoretical Computer Science},
pdf = {data/WRLA2004-13.pdf},
abstract = { The Rewriting-calculus (Rho-calculus), is a minimal framework embedding Lambda-
calculus and Term Rewriting Systems, by allowing abstraction on variables and pat-
terns. The Rho-calculus features higher-order functions (from Lambda-calculus)
and pattern-matching (from Term Rewriting Systems). In this paper, we study
extensively a second-order Rho-calculus \a la Church (RhoF) that enjoys subject
reduction, type uniqueness, and decidability of typing. We then apply a classi-
cal type-erasing function to RhoF obtaining an untyped Rho-calculus \a la Curry
(uRhoF). The related type inference system is isomorphic to RhoF and enjoys sub-
ject reduction. Both RhoF and uRhoF systems can be considered as minimal calculi
for polymorphic rewriting-based programming languages. We discuss the possibility
of a logic existing underneath the type systems via a Curry-Howard Isomorphism.
}
}

@INPROCEEDINGS{WackTCS2004,
author = {Wack,~Benjamin},
title = {The simply-typed pure pattern type
system ensures strong normalization},
year = 2004,
publisher = {IFIP-WCC TCS},
pdf = {data/rhoSN.pdf},
abstract = {  Among the various type systems that have
been proposed, the type systems of the rho-cube are especially
interesting from a logical point of view, since they extend
Barendregt's rho-cube type systems. Strong normalization,
an essential property for logical soundness, had only been
conjectured so far: in this paper, we give a positive answer
for terms typed in the first-order system of the -cube.
The proof is based on a translation of terms and types
from the rewriting calculus into the rho-calculus. First, we
deal with untyped terms, ensuring that reductions are faith-
fully mimicked in the lambda-calculus. For this, we rely on an
original encoding of the pattern matching capability of the
rho-calculus into the lambda-calculus.
Then we show how to translate types: the expressive
power of System F is needed in order to fully reproduce
the original typing judgments of the rho-calculus. We prove
that the encoding is correct with respect to reductions and
typing, and we conclude with the strong normalization of
first-order typed rho-terms.}
}

@INPROCEEDINGS{LiquoriSerpettePPDP2004,
author = {Liquori,~Luigi and Serpette,~Bernard},
title = {i{R}ho, an imperative rewriting calculus},
year = {2004},
pdf = {data/iRho.pdf},
publisher = {PPDP},
abstract = { We propose an imperative version of the Rewriting-calculus, a calculus based on pattern-
matching, pattern-abstraction, and side-effects, which we call iRho.
We formulate a static and a call-by-value dynamic semantics of iRho like that of Gilles Kahn's Natural Semantics. The operational semantics is deterministic, and immediately suggests how to build an
interpreter for the calculus. The static semantics is given via a first-order type system based on a form
of product-type, which can be assigned to iRho-terms like structures (i.e. pairs).
The calculus is \a la Church, i.e. pattern-abstractions are decorated with the types of the free variables
of the pattern.
iRho is a good candidate for a core or an intermediate language, because it can safely access and
modify a (monomorphic) typed store, and because fixed-points can be defined.
Properties like determinism of the interpreter, subject reduction, and decidability of type-checking
are completely checked by a machine assisted approach, using the Coq proof assistant. Progress and
decidability of type-checking are proved by pen and paper.}
}

@INPROCEEDINGS{rhoCalTermGraph2004,
author = {Bertolissi,~Clara and Baldan,~Paolo and Cirstea,~Horatiu and Kirchner,~Claude},
title = {{A} rewriting calculus for cyclic higher-order term graphs},
year = {2004},
pdf = {data/rhoGraphs.pdf},
publisher = {Wokshop on term graph rewriting},
abstract = {
Introduced at the end of the nineties, the Rewriting Calculus ($\rho$-calculus, for short)
is a simple calculus that fully integrates term-rewriting and -calculus. The rewrite
rules, acting as elaborated abstractions, their application and the obtained struc-
tured results are first class ob jects of the calculus. The evaluation mechanism,
generalizing beta-reduction, strongly relies on term matching in various theories.
In this paper we propose an extension of the -calculus, handling graph like
structures rather than simple terms. The transformations are performed by explicit
application of rewrite rules as first class entities. The possibility of expressing
sharing and cycles allows one to represent and compute over regular infinite entities.
The calculus over terms is naturally generalized by using unification constraints
in addition to the standard -calculus matching constraints. This therefore provides
us with the basics for a natural extension of an explicit substitution calculus to term
graphs. Several examples illustrating the introduced concepts are given.}
}

@ARTICLE{Wack06,
author = {Wack,~Benjamin},
title = {A {C}urry-{H}oward-{D}e {B}ruijn {I}somorphism {M}odulo},
institution = {LORIA},
year = {2006},
journal = {Under submission},
abstract = {   The rewriting calculus combines in a unified setting the
frameworks and capabilities of rewriting and lambda-calculus.
Its most general typed version, called Pure Pattern Type
Systems (PPTS) and adapted from Barendregt's lambda-cube, is
especially interesting from a logical point of view.
We show how to use a subset of PPTS as a proof-
term language for natural deduction modulo, extending the
Curry-Howard-De Bruijn isomorphism for this class of log-
ical formalisms. The pattern matching featured in the cal-
culus allows us to model any congruence given by a term
rewriting system.
We characterize how proofs can be denoted by PPTS
terms and we discuss the interest of our proof-term lan-
guage for the issue of cut elimination. Finally, we explore
some relations between our proof-term language and other
formalisms: extraction of lambda-terms and/or rewrite rules from
PPTS-terms, but also automated generation of proof-terms
by a rewriting-based language.},
ps = {data/wack57.pdf}
}

@ARTICLE{HOSC05,
author = {Cirstea,~Horatiu and Faure,~Germain and Kirchner,~Claude},
title = {A Rho-Calculus of explicit constraint application},
institution = {LORIA},
year = {2005},
journal = {To appear in  the journal of Higher-Order and Symbolic Computation},
abstract = {
Theoretical presentations of the rho-calculus often treat the matching constraint computations as an
atomic operation although matching constraints are explicitly expressed. Actual implementations have to take a
much more realistic view: computations needed in order to find the solutions of a matching equation can have an
important impact on the (efficiency of the) calculus for some matching theories and the substitution application
usually involves a term traversal.
Following the works on explicit substitutions in the -calculus, we present two versions of the rho-calculus, one
with explicit matching and one with explicit substitutions, together with a version that combines the two and
considers efficiency issues and more precisely the composition of substitutions. The approach is general, allowing
the extension to various matching theories. We establish the confluence of the calculus and the termination of
the explicit constraint handling and application sub-calculus.}
}

@PHDTHESIS{WackThese,
author = {Wack,~Benjamin},
title = {Typage et déduction dans le calcul de réécriture},
school = {Université Henri Poincaré - Nancy I},
year = {2005},
optkey = {},
type = {Thèse de doctorat},
month = OCT,
pdf = {data/theseBenjamin.pdf},
abstract = {The rewriting calculus is a formalism integrating functional
mechanisms from the lambda-calculus and matching capabilities from
rewriting. This thesis is devoted to the study of type systems for
this calculus, and to its applications to the domain of deduction.\\
We study the properties and the applications of two typing
paradigms. The first one is inspired by the simply typed
lambda-calculus, but it differs from it in the sense that even a
well-typed term may have a non-terminating reduction. Thus, we focus
on the use of this typed version for modeling programs, and especially
for representing rewriting systems.\\
The second family of type systems we study is adapted from the Pure
Type Systems, and features dependent types. We show the strong
normalization (which legitimates the use of the language in logic) in
two of these systems, via a translation into a lambda-calculus with
types depending on types.\\
Finally, we propose two ways of using the rewriting calculus in logic,
more particularly in relation with deduction modulo. In the first
approach, we use the systems with dependent types to define proof
terms for deduction modulo. In the second case, we define a generalization
of natural deduction and we show that a restricted form of matching is
useful in order to represent the rules of this deduction system.},
optnote = {},
optannote = {}
}

@PHDTHESIS{BertolissiThese,
author = {Bertolissi,~Clara},
title = {The graph rewriting calculus: properties and expressive capabilities},
school = {Institut National Polytechnique Lorrain - INPL},
year = {2005},
optkey = {},
type = {Thèse de doctorat},
month = OCT,
pdf = {data/theseClara.pdf},
abstract = { The last few years have seen the development of the rewriting calculus (also called rho-calculus) that uniformly integrates first-order term rewriting and lambda-calculus.
This thesis is devoted to the study of the expressiveness of the rewriting
calculus, with special interest for higher-order rewriting
and the possibility of dealing with graph-like structures.

The first part of the thesis is dedicated to the relationship between the  rewriting calculus
and higher-order term rewriting, namely the Combinatory  Reduction Systems (CRSs).
First, an original matching algorithm for CRSs terms that uses a simple term translation and the classical higher-order pattern matching of lambda terms is proposed and then
an encoding of CRSs in the rho-calculus based on a translation of each possible CRS-reduction into a corresponding rho-reduction is presented.

The second part of the thesis is devoted to an extension of the rho-calculus,
called graph rewriting calculus (or  Rg-calculus), handling terms with sharing and cycles.
The calculus over terms is naturally generalised by using unification constraints in addition to standard rho-calculus matching constraints.
The Rg-calculus is shown to be confluent over equivalence classes of terms, under
some linearity restrictions on patterns, and expressive enough to simulate
first-order term graph rewriting and cyclic lambda-calculus. }
}

@ARTICLE{RgMSCS05,
author = {Baldan,~Paolo and Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
title = {A rewriting calculus for cyclic higher-order term graphs},
institution = {Universit\'e de Venise and LORIA},
year = {2005},
journal = {To appear in  the journal of Mathematical Structures in Computer Science},
abstract = { Introduced at the end of the nineties, the Rewriting Calculus
(rho-calculus, for short) fully
integrates term-rewriting and lambda-calculus.  The rewrite
rules, acting as elaborated abstractions, their application and
the obtained structured results are first class objects of the
calculus.  The evaluation mechanism, generalising
beta-reduction, strongly relies on term matching in various
theories.
In this paper we propose an extension of the rho-calculus,
called Rg, handling structures with cycles and sharing rather
than simple terms.      This is obtained by using unification constraints in addition to
the standard rho-calculus matching constraints, which leads
to a term-graph representation in an equational style.
As for the classical RHO, the transformations are performed by
explicit application of rewrite rules as first class entities.
The possibility of expressing sharing and cycles allows one to
represent and compute over regular infinite entities.
We show that the (linear) Rg is confluent.  The proof of this
result is quite elaborated, due to the non-termination of the
system and to the fact that Rg-terms are considered modulo an
equational theory.  We also show that the Rg is expressive
enough to simulate first-order (equational) term-graph rewriting
and lambda-calculus with explicit recursion (modelled using a letrec      like construct).
}
}

@ARTICLE{CrsHOSC04,
author = {Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
title = {Expressing Combinatory Reduction Systems Derivations in the Rewriting Calculus},
institution = {LORIA},
year = {2004},
journal = {To appear in  the journal of Higher-Order and Symbolic Computation},
abstract = { The last few years have seen the development of the
rewriting calculus (also called rho-calculus or RHO) that
uniformly integrates first-order term rewriting and
lambda-calculus. The combination of these two latter formalisms
has been already handled either by enriching first-order rewriting
with higher-order capabilities, like in the Combinatory
Reduction Systems (CRS), or by adding to lambda-calculus
algebraic features. The various higher-order rewriting systems and
the rewriting calculus share similar concepts and have similar
applications, and thus, it is important to compare these
formalisms to better understand their respective strengths and
differences.

We show in this paper that we can express Combinatory Reduction
Systems derivations in terms of rewriting calculus
derivations. The approach we present is based on a translation of
each possible CRS-reduction into a corresponding
rho-reduction. Since for this purpose we need to make precise
the matching used when evaluating CRS, the second contribution of
the paper is to present an original matching algorithm for CRS    terms that uses a simple term translation and the classical
matching of lambda terms.
}
}

@INPROCEEDINGS{bertolissi05a,
crinnumber = {A05-R-413},
category = {3},
equipe = {PROTHEO},
author = {Bertolissi,~Clara},
title = {The graph rewriting calculus\,: confluence and expressiveness},
booktitle = {{9th Italian conference on Italian Conference on Theoretical Computer Science - ICTCS 2005, Siena, Italy}},
year = { 2005},
editor = {Mario Coppo, Elena Lodi, G. Michele Pinna},
volume = {3701},
series = {Lecture Notes in Computer Science},
pages = {113--127},
month = { Oct},
publisher = {Springer Verlag},
pdf = {data/rhoGraph.pdf},
abstract = {Introduced at the end of the nineties, the Rewriting Calculus (rho-calculus, for short) is a simple calculus that uniformly integrates term-rewriting and lambda-calculus. The Rhog has been recently introduced as an extension of the rho-calculus, handling structures with cycles and sharing. The calculus over terms is naturally generalized by using unification constraints in addition to the standard rho-calculus matching constraints. This leads to a term-graph representation in an equational style where terms consist of unordered lists of equations. In this paper we show that the (linear) Rhog is confluent. The proof of this result is quite elaborated, due to the non-termination of the system and to the fact that we work on equivalence classes of terms. We also show that the Rhog can be seen as a generalization of first-order term-graph rewriting, in the sense that for any term-graph rewrite step a corresponding sequence of rewritings can be found in the Rhog.}
}

@INPROCEEDINGS{FernandezM:intnrc,
author = {Fernandez,~Maribel  and Mackie,~Ian and Sinot,~Francois-Regis},
booktitle = {Proceedings of EXPRESS'05, satellite workshop of Concur},
publisher = {Elsevier},
series = {ENTCS},
title = {Interaction Nets vs. the Rho-Calculus: Introducing Bigraphical Nets},
year = {2005},
pdf = {data/rhoIN.pdf},
abstract = {
The rho-calculus generalises both term rewriting and the ¿-calculus in a uniform
framework. Interaction nets are a form of graph rewriting which proved most suc-
cessful in understanding the dynamics of the ¿-calculus, the prime example being the
implementation of optimal  beta-reduction. It is thus natural to study interaction net
encodings of the ¿-calculus as a first step towards the definition of efficient reduction
strategies. We give two interaction net encodings which bring a new understanding
to the operational semantics of the rho-calculus; however, these encodings have some
drawbacks and to overcome them we introduce bigraphical nets--a new paradigm
of computation inspired by Lafont's interactions nets and Milner's bigraphs.

}
}

@INPROCEEDINGS{CirFaurFerMacSin06,
author = {Cirstea,~Horatiu and Faure,~Germain and Fernandez,~Maribel and Mackie,~Ian and Sinot,~Francois-Regis},
booktitle = {Workshop on Reduction Strategies in Rewriting and Programming (WRS'06)},
series = {ENTCS},
title = { From Functional Programs to Interaction Nets via the Rewriting Calculus},
year = {2006},
pdf = {data/FPINrho.pdf},
abstract = {We use the rho-calculus as an intermediate language to compile functional languages with pattern-matching
features, and give an interaction net encoding of the rho-terms arising from the compilation. This encoding
gives rise to new strategies of evaluation, where pattern-matching and traditional beta-reduction can proceed
}
}

@INPROCEEDINGS{BertolissiKirchner-fossacs2007,
abstract = {The last few years have seen the development of the \emph{rewriting
calculus} (also called rho-calculus or \RHO) that uniformly integrates
first-order term rewriting and $\lambda$-calculus. The combination of
these two latter formalisms has been already handled either by enriching
first-order rewriting with higher-order capabilities, like in the
\emph{Combinatory Reduction Systems} (CRS), or by adding to
$\lambda$-calculus algebraic features.

In a previous work, the authors
showed how the semantics of CRS can be expressed in terms of the
\RHO. The converse issue is adressed here: rewriting calculus
derivations are simulated by Combinatory Reduction Systems derivations.
As a consequence of this result, important properties, like
standardisation, are deduced for the rewriting calculus.  },
author = {Bertolissi,~Clara and Kirchner,~Claude},
booktitle = {Prooceedings the FoSSaCS},
editor = {Seidl, Helmut},
month = MAR,
publisher = {Springer-Verlag},
series = {LNCS},
title = {The Rewriting Calculus as a Combinatory Reduction System},
year = {2007},
pdf = {data/bertolissiK-fossacs2007.pdf}
}

@ARTICLE{BALDAN:2006:INRIA-00110872:1,
author = {Baldan,~Paolo and Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
journal = {Mathematical Structures in Computer Science},
title = {A rewriting calculus for cyclic higher-order term graphs},
url = {https://hal.inria.fr/inria-00110872/en/},
year = {2006},
pdf = {data/rhoGraph-mscs.pdf},
abstract = {Introduced at the end of the nineties, the Rewriting Calculus
(rho-calculus, for short) fully integrates term-rewriting and
lambda-calculus.  The rewrite rules, acting as elaborated abstractions,
their application and the obtained structured results are first class
objects of the calculus.  The evaluation mechanism, generalising
beta-reduction, strongly relies on term matching in various theories.
In this paper we propose an extension of the rho-calculus, called Rg,
handling structures with cycles and sharing rather than simple terms.
This is obtained by using unification constraints in addition to the
standard rho-calculus matching constraints, which leads to a term-graph
representation in an equational style.  As for the classical RHO, the
transformations are performed by explicit application of rewrite rules
as first class entities.  The possibility of expressing sharing and
cycles allows one to represent and compute over regular infinite
entities.  We show that the (linear) Rg is confluent.  The proof of this
result is quite elaborated, due to the non-termination of the system and
to the fact that Rg-terms are considered modulo an equational theory.
We also show that the Rg is expressive enough to simulate first-order
(equational) term-graph rewriting and lambda-calculus with explicit
recursion (modelled using a letrec like construct).  }
}

@ARTICLE{CIRSTEA:2006:INRIA-00110869:1,
author = {Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
journal = {Higher-Order and Symbolic Computation},
title = {Expressing Combinatory Reduction Systems Derivations in the Rewriting Calculus},
url = {https://hal.inria.fr/inria-00110869/en/},
year = {2006},
pdf = {data/CRS2Rho.pdf},
abstract = { The last few years have seen the development of the rewriting
calculus (also called rho-calculus or RHO) that uniformly integrates
first-order term rewriting and lambda-calculus. The combination of these
two latter formalisms has been already handled either by enriching
first-order rewriting with higher-order capabilities, like in the
Combinatory Reduction Systems (CRS), or by adding to lambda-calculus
algebraic features. The various higher-order rewriting systems and the
rewriting calculus share similar concepts and have similar applications,
and thus, it is important to compare these formalisms to better
understand their respective strengths and differences.  We show in this
paper that we can express Combinatory Reduction Systems derivations in
terms of rewriting calculus derivations. The approach we present is
based on a translation of each possible CRS-reduction into a
corresponding rho-reduction. Since for this purpose we need to make
precise the matching used when evaluating CRS, the second contribution
of the paper is to present an original matching algorithm for CRS terms
that uses a simple term translation and the classical matching of lambda
terms.  }
}

@INPROCEEDINGS{CirsteaHoutmannWackWRLA2006,
author = {Cirstea,~Horatiu and Houtmann,~Clement and Wack,~Benjamin},
title = {Distributive Rho-Calculus},
booktitle = {Sixth International Workshop on Reduction Strategies in
Rewriting and Programming},
year = {2006},
month = {Apr},
note = {accepted},
pdf = {data/distrib-wrla2006.pdf},
abstract = {
The rewriting calculus has been introduced as a general formalism that uniformly
integrates rewriting and  lambda-calculus. In this calculus all the basic ingredients of
rewriting such as rewrite rules, rule applications and results are first-class objects.
The rewriting calculus has been originally designed and used for expressing the
semantics of rule based as well as object oriented paradigms. We have previously
shown that convergent term rewriting systems and classic strategies can be encoded
naturally in the calculus.
In this paper, we go a step further and we propose an extended version of the
calculus that allows one to encode unrestricted term rewriting systems. This version
of the calculus features a new evaluation rule describing the behavior of the result
structures and a call-by-value evaluation strategy. We prove the confluence of the
obtained calculus and the correctness and completeness of the proposed encoding.
}
}

@INPROCEEDINGS{CirsteaF07,
title = {Confluence of pattern-based lambda-calculi},
author = {Horatiu Cirstea and Germain Faure},
booktitle = {Rewriting Techniques and Applications},
year = {2007},
volume = {4533},
pages = {78--92},
pdf = {data/rta07.pdf},
abstract = {
Different pattern calculi integrate the functional mechanisms from the
\lambda-calculus and the matching capabilities from rewriting.
Several approaches are  used to obtain the confluence but  in practice the proof
methods share
the same structure and  each variation on the way
pattern-abstractions are applied needs another proof of confluence.

In this paper, we propose a generic confluence proof where the way
pattern-abstractions are applied is axiomatized. Intuitively, the conditions
guarantee that  the matching is stable by substitution and by reduction.

We show that our approach directly applies to different pattern
calculi, namely the lambda calculus with patterns, the pure pattern
calculus and the rewriting calculus.
We also characterize a class of matching algorithms and consequently
of pattern-calculi that are not confluent.
}
}

@INPROCEEDINGS{faureM07,
title = {A Categorical Semantics of The Parallel Lambda-Calculus},
author = {Germain Faure and Alexandre Miquel},
year = {2007},
volume = {Submited},
pdf = {data/lics07.pdf},
abstract = {In this paper, we define a sound and complete categorical semantics
for the parallel lambda-calculus, based on a notion of
aggregation monad which is modular w.r.t. associativity,
commutativity and idempotence.

To prove completeness, we introduce a category of partial
equivalence relations adapted to parallelism, in which any
extension of the basic equational theory of the calculus is induced
by some model.

We also present abstract methods to construct models of the
parallel lambda-calculus in categories where particular
equations have solutions, such as the category of Scott domains and
its variants, and check that G. Boudol's original semantics is a
particular case of ours.}
}
`

This file has been generated by bibtex2html 1.86.