RhoCalculus Papers
One can either browse the raw list of publications or follow the guidelines below.
The syntax and semantics of the calculus can be found in different papers but a good starting point is the "Rewriting Calculus with Fixpoints" [CLW03] that presents not only the untyped calculus but also a firstorder type system suitable for programming purposes. Different operational semantics for this calculus can be found in the overview paper "Rewriting calculus with(out) types" [CKL02].
Several extensions have been proposed for the rhocalculus: a versions handling explicitly the (application of) constraints [CFK04] and [CFK05], a (typed) imperative version of the calculus [LS04] and the corresponding certified interpreter, a version generalizing the patterns from terms to graphs [BBCK04]. The calculus has been also compared to higherorder rewriting and more precisely to CRS [BCK03].
A polymorphic type system can be found in the previously mentioned paper "Rewriting calculus with(out) types" [CKL02] and type checking and type inference issues have been studied in [LW04]. The approach is extended to "Pure patterns type systems" (PPTS) [BCKL03] (the syntax used here is slightly different from the classical one), a generalization of Pure type systems for the rhocalculus. It has been shown that "The simplytyped pure pattern type system ensures strong normalization" [Wac04].
The starting point of PPTS comes from "The Rho Cube" [CKL01b]. The syntax and the semantics of the rhocalculus used here are slightly different from the latest version. The same syntax is used for showing the "Matching Power" [CKL01a], that is the way rhocalculus can encode different (object) calculi.
The syntax and semantics used in these two papers can be seen as the simplification of the initial version of "The Rewriting Calculus" [CK01b,CK01c]. These papers present extensively the initial design of the calculus and the transition to the latest version is presented in [CKLW03]. Several papers present the way this initial version can be used for giving a semantics to rewrite based languages [CK98a,CK98b,CK98c] or other formalisms [CK01a,CK00a]. A simple type system [CK00b] has been introduced and an exception mechanism has been studied [FK02].
There are several reports giving more details on the different topics
enumerated above. The PhD thesis of Horatiu Cirstea [Cir00]
presents the initial version of the calculus, the master thesis of
Clara Bertolissi [Ber02] present the relationship with CRS, the
master thesis of Benjamin Wack [Wac02] deals with the typed
aspects of the calculus, the master thesis of Germain
Faure [Fau03] gives more details on the explicit rhocalculus
and its report [Fau01] presents the way exceptions can be
handled in rhocalculus.
[FM07] 
Germain Faure and Alexandre Miquel.
A categorical semantics of the parallel lambdacalculus.
volume Submited, 2007.
[ bib 
.pdf ]
In this paper, we define a sound and complete categorical semantics for the parallel lambdacalculus, based on a notion of aggregation monad which is modular w.r.t. associativity, commutativity and idempotence.

[CF07] 
Horatiu Cirstea and Germain Faure.
Confluence of patternbased lambdacalculi.
In Rewriting Techniques and Applications, volume 4533, pages
7892, 2007.
[ bib 
.pdf ]
Different pattern calculi integrate the functional mechanisms from the λ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 patternabstractions are applied needs another proof of confluence.

[CHW06] 
Horatiu Cirstea, Clement Houtmann, and Benjamin Wack.
Distributive rhocalculus.
In Sixth International Workshop on Reduction Strategies in
Rewriting and Programming, Vienna (Austria), Apr 2006.
accepted.
[ bib 
.pdf ]
The rewriting calculus has been introduced as a general formalism that uniformly integrates rewriting and lambdacalculus. In this calculus all the basic ingredients of rewriting such as rewrite rules, rule applications and results are firstclass 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 callbyvalue evaluation strategy. We prove the confluence of the obtained calculus and the correctness and completeness of the proposed encoding.

[BCK06] 
Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner.
Expressing combinatory reduction systems derivations in the rewriting
calculus.
HigherOrder and Symbolic Computation, 2006.
[ bib 
http 
.pdf ]
The last few years have seen the development of the rewriting calculus (also called rhocalculus or RHO) that uniformly integrates firstorder term rewriting and lambdacalculus. The combination of these two latter formalisms has been already handled either by enriching firstorder rewriting with higherorder capabilities, like in the Combinatory Reduction Systems (CRS), or by adding to lambdacalculus algebraic features. The various higherorder 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 CRSreduction into a corresponding rhoreduction. 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.

[BBCK06] 
Paolo Baldan, Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner.
A rewriting calculus for cyclic higherorder term graphs.
Mathematical Structures in Computer Science, 2006.
[ bib 
http 
.pdf ]
Introduced at the end of the nineties, the Rewriting Calculus (rhocalculus, for short) fully integrates termrewriting and lambdacalculus. 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 betareduction, strongly relies on term matching in various theories. In this paper we propose an extension of the rhocalculus, called Rg, handling structures with cycles and sharing rather than simple terms. This is obtained by using unification constraints in addition to the standard rhocalculus matching constraints, which leads to a termgraph 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 nontermination of the system and to the fact that Rgterms are considered modulo an equational theory. We also show that the Rg is expressive enough to simulate firstorder (equational) termgraph rewriting and lambdacalculus with explicit recursion (modelled using a letrec like construct).

[BK07] 
Clara Bertolissi and Claude Kirchner.
The rewriting calculus as a combinatory reduction system.
In Helmut Seidl, editor, Prooceedings the FoSSaCS, LNCS, Braga,
Portugal, March 2007. SpringerVerlag.
[ bib 
.pdf ]
The last few years have seen the development of the rewriting calculus (also called rhocalculus or ) that uniformly integrates firstorder term rewriting and λcalculus. The combination of these two latter formalisms has been already handled either by enriching firstorder rewriting with higherorder capabilities, like in the Combinatory Reduction Systems (CRS), or by adding to λcalculus algebraic features.

[CFF^{+}06] 
Horatiu Cirstea, Germain Faure, Maribel Fernandez, Ian Mackie, and
FrancoisRegis Sinot.
From functional programs to interaction nets via the rewriting
calculus.
In Workshop on Reduction Strategies in Rewriting and Programming
(WRS'06), ENTCS, 2006.
[ bib 
.pdf ]
We use the rhocalculus as an intermediate language to compile functional languages with patternmatching features, and give an interaction net encoding of the rhoterms arising from the compilation. This encoding gives rise to new strategies of evaluation, where patternmatching and traditional betareduction can proceed in parallel without overheads.

[FMS05] 
Maribel Fernandez, Ian Mackie, and FrancoisRegis Sinot.
Interaction nets vs. the rhocalculus: Introducing bigraphical nets.
In Proceedings of EXPRESS'05, satellite workshop of Concur,
ENTCS. Elsevier, 2005.
[ bib 
.pdf ]
The rhocalculus 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 betareduction. 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 rhocalculus; however, these encodings have some drawbacks and to overcome them we introduce bigraphical netsa new paradigm of computation inspired by Lafont's interactions nets and Milner's bigraphs.

[Ber05a] 
Clara Bertolissi.
The graph rewriting calculus: confluence and expressiveness.
In G. Michele Pinna Mario Coppo, Elena Lodi, editor, 9th
Italian conference on Italian Conference on Theoretical Computer Science 
ICTCS 2005, Siena, Italy, volume 3701 of Lecture Notes in Computer
Science, pages 113127. Springer Verlag, Oct 2005.
[ bib 
.pdf ]
Introduced at the end of the nineties, the Rewriting Calculus (rhocalculus, for short) is a simple calculus that uniformly integrates termrewriting and lambdacalculus. The Rhog has been recently introduced as an extension of the rhocalculus, handling structures with cycles and sharing. The calculus over terms is naturally generalized by using unification constraints in addition to the standard rhocalculus matching constraints. This leads to a termgraph 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 nontermination 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 firstorder termgraph rewriting, in the sense that for any termgraph rewrite step a corresponding sequence of rewritings can be found in the Rhog.

[BCK04] 
Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner.
Expressing combinatory reduction systems derivations in the rewriting
calculus.
To appear in the journal of HigherOrder and Symbolic
Computation, 2004.
[ bib ]
The last few years have seen the development of the rewriting calculus (also called rhocalculus or RHO) that uniformly integrates firstorder term rewriting and lambdacalculus. The combination of these two latter formalisms has been already handled either by enriching firstorder rewriting with higherorder capabilities, like in the Combinatory Reduction Systems (CRS), or by adding to lambdacalculus algebraic features. The various higherorder 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.

[BBCK05] 
Paolo Baldan, Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner.
A rewriting calculus for cyclic higherorder term graphs.
To appear in the journal of Mathematical Structures in Computer
Science, 2005.
[ bib ]
Introduced at the end of the nineties, the Rewriting Calculus (rhocalculus, for short) fully integrates termrewriting and lambdacalculus. 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 betareduction, strongly relies on term matching in various theories. In this paper we propose an extension of the rhocalculus, called Rg, handling structures with cycles and sharing rather than simple terms. This is obtained by using unification constraints in addition to the standard rhocalculus matching constraints, which leads to a termgraph 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 nontermination of the system and to the fact that Rgterms are considered modulo an equational theory. We also show that the Rg is expressive enough to simulate firstorder (equational) termgraph rewriting and lambdacalculus with explicit recursion (modelled using a letrec like construct).

[Ber05b] 
Clara Bertolissi.
The graph rewriting calculus: properties and expressive
capabilities.
Thèse de doctorat, Institut National Polytechnique Lorrain  INPL,
October 2005.
[ bib 
.pdf ]
The last few years have seen the development of the rewriting calculus (also called rhocalculus) that uniformly integrates firstorder term rewriting and lambdacalculus. This thesis is devoted to the study of the expressiveness of the rewriting calculus, with special interest for higherorder rewriting and the possibility of dealing with graphlike structures.

[Wac05] 
Benjamin Wack.
Typage et déduction dans le calcul de réécriture.
Thèse de doctorat, Université Henri Poincaré  Nancy I, October 2005.
[ bib 
.pdf ]
The rewriting calculus is a formalism integrating functional mechanisms from the lambdacalculus 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.

[CFK05] 
Horatiu Cirstea, Germain Faure, and Claude Kirchner.
A rhocalculus of explicit constraint application.
To appear in the journal of HigherOrder and Symbolic
Computation, 2005.
[ bib ]
Theoretical presentations of the rhocalculus 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 rhocalculus, 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 subcalculus.

[Wac06] 
Benjamin Wack.
A CurryHowardDe Bruijn Isomorphism Modulo.
Under submission, 2006.
[ bib 
.pdf ]
The rewriting calculus combines in a unified setting the frameworks and capabilities of rewriting and lambdacalculus. Its most general typed version, called Pure Pattern Type Systems (PPTS) and adapted from Barendregt's lambdacube, 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 CurryHowardDe 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 proofterm lan guage for the issue of cut elimination. Finally, we explore some relations between our proofterm language and other formalisms: extraction of lambdaterms and/or rewrite rules from PPTSterms, but also automated generation of proofterms by a rewritingbased language.

[BBCK04] 
Clara Bertolissi, Paolo Baldan, Horatiu Cirstea, and Claude Kirchner.
A rewriting calculus for cyclic higherorder term graphs.
Wokshop on term graph rewriting, 2004.
[ bib 
.pdf ]
Introduced at the end of the nineties, the Rewriting Calculus (ρcalculus, for short) is a simple calculus that fully integrates termrewriting 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 betareduction, 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.

[LS04] 
Luigi Liquori and Bernard Serpette.
iRho, an imperative rewriting calculus.
PPDP, 2004.
[ bib 
.pdf ]
We propose an imperative version of the Rewritingcalculus, a calculus based on pattern matching, patternabstraction, and sideeffects, which we call iRho. We formulate a static and a callbyvalue 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 firstorder type system based on a form of producttype, which can be assigned to iRhoterms like structures (i.e. pairs). The calculus is à la Church, i.e. patternabstractions 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 fixedpoints can be defined. Properties like determinism of the interpreter, subject reduction, and decidability of typechecking are completely checked by a machine assisted approach, using the Coq proof assistant. Progress and decidability of typechecking are proved by pen and paper.

[Wac04] 
Benjamin Wack.
The simplytyped pure pattern type system ensures strong
normalization.
IFIPWCC TCS, 2004.
[ bib 
.pdf ]
Among the various type systems that have been proposed, the type systems of the rhocube are especially interesting from a logical point of view, since they extend Barendregt's rhocube 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 firstorder system of the cube. The proof is based on a translation of terms and types from the rewriting calculus into the rhocalculus. First, we deal with untyped terms, ensuring that reductions are faith fully mimicked in the lambdacalculus. For this, we rely on an original encoding of the pattern matching capability of the rhocalculus into the lambdacalculus. 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 rhocalculus. We prove that the encoding is correct with respect to reductions and typing, and we conclude with the strong normalization of firstorder typed rhoterms.

[LW04] 
Luigi Liquori and Benjamin Wack.
The polymorphic rewritingcalculus [type checking vs. type
inference].
In Proceedings of the 5th workshop on rewriting logic and
applications. vol. 117 of Electronic Notes in Theoretical Computer Science,
2004.
[ bib 
.pdf ]
The Rewritingcalculus (Rhocalculus), is a minimal framework embedding Lambda calculus and Term Rewriting Systems, by allowing abstraction on variables and pat terns. The Rhocalculus features higherorder functions (from Lambdacalculus) and patternmatching (from Term Rewriting Systems). In this paper, we study extensively a secondorder Rhocalculus à la Church (RhoF) that enjoys subject reduction, type uniqueness, and decidability of typing. We then apply a classi cal typeerasing function to RhoF obtaining an untyped Rhocalculus à 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 rewritingbased programming languages. We discuss the possibility of a logic existing underneath the type systems via a CurryHoward Isomorphism.

[CFK04] 
Horatiu Cirstea, Germain Faure, and Claude Kirchner.
A rhocalculus of explicit constraint application.
In Proceedings of the 5th workshop on rewriting logic and
applications. vol. 117 of Electronic Notes in Theoretical Computer Science,
2004.
[ bib 
.pdf ]
Theoretical presentations of the rhocalculus 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 λcalculus, we propose, study and exemplify a rhocalculus 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 subcalculus.

[CLW03] 
Horatiu Cirstea, Luigi Liquori, and Benjamin Wack.
Rewriting calculus with fixpoints: Untyped and firstorder systems.
volume 3085. Springer, 2003.
[ bib 
.pdf ]
The rewriting calculus, also called rhocalculus, is a framework embed ding lambdacalculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higherorder mechanisms of the lambdacalculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for the lambdacalculus can be generalized to the rhocalculus: in this paper, we study extensively a firstorder rhocalculus à 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 rewritingbased language.

[BCK03] 
Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner.
Translating Combinatory Reduction Systems into the Rewriting
Calculus.
In JeanLouis Giavitto and PierreEtienne Moreau, editors,
Proceedings of the 4th International Workshop on RuleBased Programming
Valencia, Spain, June 9, 2003, Valencia, Spain, June 2003. Electronic Notes
in Theoretical Computer Science.
[ bib 
.pdf ]
The last few years have seen the development of the rewriting calculus (or rhocalculus, RHO) that extends first order term rewriting and λcalculus. The integration of these two latter formalisms has been already handled either by enriching firstorder rewriting with higherorder capabilities, like in the Combinatory Reduction Systems, or by adding to λcalculus algebraic features. The different higherorder 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 CRSterms and rewrite rules into rhoterms and we show that for any CRSreduction we have a corresponding rhoreduction.

[Wac03] 
Benjamin Wack.
Klop counter example in the rhocalculus.
Draft notes, LORIA, Nancy, 2003.
[ bib 
.pdf ]
We give a rhotranslation of Klop's classical example about nonconfluence for higherorder systems with nonlinear matching.

[Fau03] 
Germain Faure.
Explicit rewriting calculus.
Master thesis, ENSCachan,IRISA,LORIA, Sep 2003.
[ bib 
.pdf ]
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 lambdacalculus 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.

[CKLW03] 
Horatiu Cirstea, Claude Kirchner, Luigi Liquori, and Benjamin Wack.
Rewrite strategies in the rewriting calculus.
In Bernhard Gramlich and Salvador Lucas, editors, Proceedings
of the Third International Workshop on Reduction Strategies in Rewriting and
Programming , Valencia, Spain, June 2003. Electronic Notes in Theoretical
Computer Science.
[ bib 
.pdf ]
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.

[BCKL03] 
Gilles Barthe, Horatiu Cirstea, Claude Kirchner, and Luigi Liquori.
Pure patterns type systems.
In Principles of Programming Languages  POPL2003, New
Orleans, USA. ACM, January 2003.
[ bib 
.pdf ]
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 builtin matching facilities. This framework, that we call “Pure Pattern Type Systems”, is particularly wellsuited for the foundations of programming (meta)languages and proof assistants since it provides in a fully unified setting higherorder 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 CurryHoward isomorphism.

[CKL02] 
Horatiu Cirstea, Claude Kirchner, and Luigi Liquori.
Rewriting calculus with(out) types.
In Fabio Gadducci and Ugo Montanari, editors, Proceedings of the
fourth workshop on rewriting logic and applications, Pisa (Italy), September
2002. Electronic Notes in Theoretical Computer Science.
[ bib 
.pdf ]
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, associativitycommutativity, 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 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 CurryHoward isomorphism.

[Ber02] 
Clara Bertolissi.
dea.
Rapport de dea, LORIA, Nancy, July 2002.
[ bib 
.pdf ]
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.

[CKLW02] 
Horatiu Cirstea, Claude Kirchner, Luigi Liquori, and Benjamin Wack.
The rewriting calculus : some results, some problems.
In Delia Kesner, Femke van Raamsdonk, and Tobias Nipkow, editors,
The first international workshop on HigherOrder Rewriting, pages
1  2, Copenhagen, Denmark, July 2002. FLoC'02.
[ bib 
.ps ]
The rewriting calculus, also called rhocalculus, embeds in a same setting the lambdacalculus and the rewriting, by allowing abstraction not only on variables but also on patterns. The higherorder mechanisms of the lambdacalculus 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 rhocalculus as an extension of the lambdacalculus, and we study the typed aspects. Our study is based upon a generalization of Barendregt's lambdacube, in which we unify both abstractors lambda and Pi into a single one. We need to deal with the original features of the rhocalculus too: matching power, nondeterminism, 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.

[Wac02] 
Benjamin Wack.
Aspects typés du calcul de réécriture.
Rapport de dea, LORIA  ENS Lyon, Nancy, July 2002.
[ bib 
.pdf ]
Le calcul de réécriture, ou rhocalcul, intègre dans un même système le lambdacalcul 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 lambdacalcul 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 rhocalcul en tant qu'extension du lambdacalcul 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 rhocalcul : puissance du filtrage, nondé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.

[Fau01] 
Germain Faure.
Etude des propriétés du calcul de réécriture: du rho au
rhoepsilon calcul.
Rapport du stage de première année du magistère d'informatique et
de modélisation de l'ens lyon, LORIA et ENS Lyon, Nancy, September 2001.
[ bib 
.pdf ]
Abstract html/rhoGermainresume.htmlin French, or html/rhoGermainabstract.htmlin English

[FK02] 
Germain Faure and Claude Kirchner.
Exceptions in the rewriting calculus.
In Sophie Tison, editor, Proceedings of the RTA conference,
volume 2378 of Lecture Notes in Computer Science, pages 6682,
Copenhagen, July 2002. SpringerVerlag.
[ bib 
.pdf ]
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.

[CK01a]  Horatiu Cirstea and Claude Kirchner. Rewriting and Multisets in Rhocalculus and ELAN. Romanian Journal of Information, Science and Technology, 4(12):3348, 2001. ISSN: 14538245. [ bib  .pdf ] 
[CK00a] 
Horatiu Cirstea and Claude Kirchner.
Rewriting and multisets in the rewriting calculus and elan.
In Workshop on Multiset Processing, Curtea de Arges, Romania,
Aug 2000.
[ bib 
.pdf ]
The rewriting calculus is a new calculus that integrates in a uniform and simple setting firstorder rewriting, lambdacalculus and nondeterministic 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 firstorder conditional rewriting and lambdacalculus and it can be used in order to give an operational semantics to the rewrite based language Elan. We show how the setlike data structures are easily represented in Elan and how this can be used in order to specify protocols.

[BKRK01] 
Peter Borovansky, Claude Kirchner, Christophe Ringeissen, and Helene Kirchner.
Rewriting with strategies in ELAN: a functional semantics.
International Journal of Foundations of Computer Science,
12(1):6998, February 2001.
[ bib 
.pdf ]
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 higherorder 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 ELAN is illustrated by examples of polymorphic functions and strategies.

[CK01c]  Horatiu Cirstea and Claude Kirchner. The rewriting calculus  Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics, 9(3):427498, May 2001. [ bib ] 
[CK01d] 
Horatiu Cirstea and Claude Kirchner.
The rewriting calculus  Part II.
Logic Journal of the Interest Group in Pure and Applied Logics,
9(3):465498, May 2001.
[ bib 
.pdf ]
The Rhocalculus integrates in a uniform and simple setting firstorder rewriting, Lambdacalculus and nondeterministic 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 rhocalculus. This second part is first devoted to the use of the rhocalculus 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 rhocalculus.

[CK01b] 
Horatiu Cirstea and Claude Kirchner.
The rewriting calculus  Part I.
Logic Journal of the Interest Group in Pure and Applied Logics,
9(3):427463, May 2001.
[ bib 
.pdf ]
The Rhocalculus integrates in a uniform and simple setting firstorder rewriting, Lambdacalculus and nondeterministic 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 Lambdacalculus as well as firstorder 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 Lambdacalculus. 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.

[CKL01b] 
Horatiu Cirstea, Claude Kirchner, and Luigi Liquori.
The Rho Cube.
In Furio Honsell, editor, Foundations of Software Science and
Computation Structures, http://www.disi.unige.it/etaps2001ETAPS'2001,
http://www.springer.de/comp/lncs/index.htmlLecture Notes in Computer
Science, pages 166180, Genova, Italy, April 2001. SpringerVerlag©.
[ bib 
.pdf ]
The rewriting calculus, or Rho Calculus, is a simple calculus that uniformly integrates abstraction on patterns and nondeterminism. Therefore, it fully integrates rewriting and Lambdacalculus. 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 Rhocube that extends the Lambdacube 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 Rhoversions of the Logical Framework of HarperHonsellPlotkin, and of the Calculus of Constructions of CoquandHuet.

[Cir00] 
Horatiu Cirstea.
Calcul de réécriture : fondements et applications.
PhD thesis, Université Henri Poincaré  Nancy I, 2000.
October 25.
[ bib 
.pdf ]
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 rhocalcul, qui généralise la réécriture du premier ordre et le lambdacalcul tout en permettant d'exprimer le nondé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 nondé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 lambdacalcul. Le calcul de réécriture n'est pas terminant dans le cas nontypé 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 innermost et 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 ELAN, un langage basé sur l'application de règles de réécriture contrôlées par des stratégies.

[CKL01a] 
Horatiu Cirstea, Claude Kirchner, and Luigi Liquori.
Matching Power.
In Proceedings of RTA'2001, Lecture Notes in Computer
Science. SpringerVerlag, May 2001.
[ bib 
.pdf ]
In this paper we give a simple and uniform presentation of the rewriting calculus, also called rhocalculus. 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 rhocalculus 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.

[CK00b] 
Horatiu Cirstea and Claude Kirchner.
The typed rewriting calculus.
In Third International Workshop on Rewriting Logic and
Application, Kanazawa (Japan), September 2000.
[ bib 
.pdf ]
The rewriting calculus is a rule construction and application framework. As such it embeds in a uniform way term rewriting and lambdacalculus. 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.

[CK98b]  Horatiu Cirstea and Claude Kirchner. The rewriting calculus as a semantics of ELAN. In J. Hsiang and A. Ohori, editors, 4th Asian Computing Science Conference, volume 1538 of Lecture Notes in Computer Science, pages 810, Manila, The Philippines, December 1998. SpringerVerlag. [ bib  .pdf ] 
[CK98a]  Horatiu Cirstea and Claude Kirchner. Combining higherorder and firstorder computation using ρcalculus: Towards a semantics of ELAN. In Dov Gabbay and Maarten de Rijke, editors, Frontiers of Combining Systems 2, Research Studies, ISBN 0863802524, appeared in 1999, pages 95120. Wiley, October 1998. [ bib ] 
[CK99] 
Horatiu Cirstea and Claude Kirchner.
An introduction to the rewriting calculus.
Research Report RR3818, INRIA, December 1999.
[ bib 
.html ]
The rhocalculus is a new calculus that integrates in a uniform and simple setting firstorder rewriting, lambdacalculus and nondeterministic computations. This report describes the calculus from its syntax to its basic properties in the untyped case. We show how it embeds firstorder conditional rewriting and lambdacalculus. Finally we use the rhocalculus to give an operational semantics to the rewrite based language ELAN.

[CK98c]  Horatiu Cirstea and Claude Kirchner. ρcalculus. Its Syntax and Basic Properties. In Workshop CCL'98, Jerusalem, Israel, September 1998. [ bib  .pdf ] 
This file has been generated by bibtex2html 1.86.