Rho-Calculus 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 first-order 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 rho-calculus: 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 higher-order 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 rho-calculus. It has been shown that "The simply-typed 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 rho-calculus used here are slightly different from the latest version. The same syntax is used for showing the "Matching Power" [CKL01a], that is the way rho-calculus 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 rho-calculus and its report [Fau01] presents the way exceptions can be handled in rho-calculus.

papers

[FM07]	Germain Faure and Alexandre Miquel. A categorical semantics of the parallel lambda-calculus. volume Submited, 2007. [ bib \| .pdf ] 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.
[CF07]	Horatiu Cirstea and Germain Faure. Confluence of pattern-based lambda-calculi. In Rewriting Techniques and Applications, volume 4533, pages 78-92, 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 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.
[CHW06]	Horatiu Cirstea, Clement Houtmann, and Benjamin Wack. Distributive rho-calculus. 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 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.
[BCK06]	Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner. Expressing combinatory reduction systems derivations in the rewriting calculus. Higher-Order and Symbolic Computation, 2006. [ bib \| http \| .pdf ] 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.
[BBCK06]	Paolo Baldan, Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner. A rewriting calculus for cyclic higher-order term graphs. Mathematical Structures in Computer Science, 2006. [ bib \| http \| .pdf ] 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).
[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. Springer-Verlag. [ bib \| .pdf ] The last few years have seen the development of the rewriting calculus (also called rho-calculus or ) that uniformly integrates first-order term rewriting and λ-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 λ-calculus algebraic features. In a previous work, the authors showed how the semantics of CRS can be expressed in terms of the . 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.
[CFF⁺06]	Horatiu Cirstea, Germain Faure, Maribel Fernandez, Ian Mackie, and Francois-Regis 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 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 in parallel without overheads.
[FMS05]	Maribel Fernandez, Ian Mackie, and Francois-Regis Sinot. Interaction nets vs. the rho-calculus: Introducing bigraphical nets. In Proceedings of EXPRESS'05, satellite workshop of Concur, ENTCS. Elsevier, 2005. [ bib \| .pdf ] 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.
[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 113-127. Springer Verlag, Oct 2005. [ bib \| .pdf ] 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.
[BCK04]	Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner. Expressing combinatory reduction systems derivations in the rewriting calculus. To appear in the journal of Higher-Order and Symbolic Computation, 2004. [ bib ] 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.
[BBCK05]	Paolo Baldan, Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner. A rewriting calculus for cyclic higher-order 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 (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).
[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 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.
[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 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.
[CFK05]	Horatiu Cirstea, Germain Faure, and Claude Kirchner. A rho-calculus of explicit constraint application. To appear in the journal of Higher-Order and Symbolic Computation, 2005. [ bib ] 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.
[Wac06]	Benjamin Wack. A Curry-Howard-De Bruijn Isomorphism Modulo. Under submission, 2006. [ bib \| .pdf ] 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.
[BBCK04]	Clara Bertolissi, Paolo Baldan, Horatiu Cirstea, and Claude Kirchner. A rewriting calculus for cyclic higher-order 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 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.
[LS04]	Luigi Liquori and Bernard Serpette. iRho, an imperative rewriting calculus. PPDP, 2004. [ bib \| .pdf ] 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 à 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.
[Wac04]	Benjamin Wack. The simply-typed pure pattern type system ensures strong normalization. IFIP-WCC TCS, 2004. [ bib \| .pdf ] 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.
[LW04]	Luigi Liquori and Benjamin Wack. The polymorphic rewriting-calculus [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 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 à 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 à 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.
[CFK04]	Horatiu Cirstea, Germain Faure, and Claude Kirchner. A rho-calculus 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 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 λ-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.
[CLW03]	Horatiu Cirstea, Luigi Liquori, and Benjamin Wack. Rewriting calculus with fixpoints: Untyped and first-order systems. volume 3085. Springer, 2003. [ bib \| .pdf ] 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 à 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.
[BCK03]	Clara Bertolissi, Horatiu Cirstea, and Claude Kirchner. Translating Combinatory Reduction Systems into the Rewriting Calculus. In Jean-Louis Giavitto and Pierre-Etienne Moreau, editors, Proceedings of the 4th International Workshop on Rule-Based 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 rho-calculus, RHO) that extends first order term rewriting and λ-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 Combinatory Reduction Systems, or by adding to λ-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.
[Wac03]	Benjamin Wack. Klop counter example in the rho-calculus. Draft notes, LORIA, Nancy, 2003. [ bib \| .pdf ] We give a rho-translation of Klop's classical example about non-confluence for higher-order systems with non-linear matching.
[Fau03]	Germain Faure. Explicit rewriting calculus. Master thesis, ENS-Cachan,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 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.
[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 built-in matching facilities. This framework, that we call “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.
[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, 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 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.
[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 Higher-Order Rewriting, pages 1 - 2, Copenhagen, Denmark, July 2002. FLoC'02. [ bib \| .ps ] 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.
[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 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.
[Fau01]	Germain Faure. Etude des propriétés du calcul de r��criture: du rho au rho-epsilon 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/rhoGermain-resume.htmlin French, or html/rhoGermain-abstract.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 66-82, Copenhagen, July 2002. Springer-Verlag. [ 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 Rho-calculus and ELAN. Romanian Journal of Information, Science and Technology, 4(1-2):33-48, 2001. ISSN: 1453-8245. [ 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 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.
[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):69-98, 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 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 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):427-498, 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):465-498, May 2001. [ bib \| .pdf ] 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.
[CK01b]	Horatiu Cirstea and Claude Kirchner. The rewriting calculus - Part I. Logic Journal of the Interest Group in Pure and Applied Logics, 9(3):427-463, May 2001. [ bib \| .pdf ] 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.
[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 166-180, Genova, Italy, April 2001. Springer-Verlag�. [ bib \| .pdf ] 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.
[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 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 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. Springer-Verlag, May 2001. [ bib \| .pdf ] 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.
[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 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.
[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 8-10, Manila, The Philippines, December 1998. Springer-Verlag. [ bib \| .pdf ]
[CK98a]	Horatiu Cirstea and Claude Kirchner. Combining higher-order and first-order 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 95-120. Wiley, October 1998. [ bib ]
[CK99]	Horatiu Cirstea and Claude Kirchner. An introduction to the rewriting calculus. Research Report RR-3818, INRIA, December 1999. [ bib \| .html ] 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.
[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.