papers.bib

@INPROCEEDINGS{CirsteaKirchnerCCL98,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {$\rho$-calculus. {I}ts {S}yntax and {B}asic {P}roperties},
  year = {1998},
  pdf = {data/ccl98.pdf},
  booktitle = {Workshop CCL'98},
  address = {Jerusalem, Israel},
  month = SEP
}
@TECHREPORT{CirsteaKirchnerINRIA99,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {An introduction to the rewriting calculus},
  institution = {INRIA},
  month = DEC,
  number = {RR-3818},
  type = {Research Report},
  year = {1999},
  url = {http://www.inria.fr/rrrt/rr-3818.html},
  abstract = {The rho-calculus is a new calculus that integrates
	in a uniform and simple setting first-order rewriting,
	lambda-calculus and non-deterministic computations. This
	report describes the calculus from its syntax to its basic
	properties in the untyped case. We show how it embeds
	first-order conditional rewriting and lambda-calculus. Finally
	we use the rho-calculus to give an operational semantics to
	the rewrite based language ELAN.}
}
@INCOLLECTION{CirsteaKirchner-LivreFroCoS99,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {Combining Higher-Order and First-Order Computation Using
                 $\rho$-calculus: Towards a semantics of {{\sf ELAN}}},
  booktitle = {Frontiers of Combining Systems 2},
  publisher = {Wiley},
  year = {1998},
  month = OCT,
  editor = {Gabbay, Dov and de Rijke, Maarten},
  series = {Research Studies, ISBN 0863802524, appeared in 1999},
  pages = {95--120},
  comment = {Invited presentation by CK}
}
@INPROCEEDINGS{CirsteaKirchner-Asian98,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {The rewriting calculus as a semantics of {{\sf ELAN}}},
  booktitle = {{4th Asian Computing Science Conference}},
  editor = {Hsiang, J. and Ohori, A.},
  year = {1998},
  pdf = {data/asian98.pdf},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = 1538,
  month = DEC,
  pages = {8--10},
  address = {Manila, The Philippines},
  comment = {Invited presentation by CK}
}
@INPROCEEDINGS{CirsteaKirchnerWRLA2000,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {The Typed Rewriting Calculus},
  year = {2000},
  booktitle = {Third International Workshop on Rewriting Logic and 
		     Application },
  address = {Kanazawa (Japan)},
  month = SEP,
  pdf = {data/wrla2000.pdf},
  abstract = {The rewriting calculus is a rule construction and
	application framework. As such it embeds in a uniform way term
	rewriting and lambda-calculus. Since rule application is an
	explicit object of the calculus, it allows us also to handle
	the set of results explicitly.
	We present a simply typed version of the rewriting
	calculus. With a good choice of the type system, we show that
	the calculus is type preserving and terminating, i.e. verifies
	the subject reduction and strong normalization properties.
	}
}
@INPROCEEDINGS{CirsteaKirchnerLiquoriMatchingPower-RTA2001,
  author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi},
  title = {{M}atching {P}ower},
  year = {2001},
  booktitle = {Proceedings of {RTA'2001}},
  publisher = {Springer-Verlag},
  series = {{Lecture Notes in Computer Science}},
  month = MAY,
  ps = {data/rta2001.pdf},
  abstract = {In this paper we give a simple and uniform
	presentation of the rewriting calculus, also called
	rho-calculus.  In addition to its simplicity, this formulation
computations	explicitly allows us to encode complex structures such as
	lists, sets, and objects.  We provide extensive examples of
	the calculus, and we focus on its ability to represent some
	object oriented calculi, namely the Lambda Calculus of Objects
	of Fisher, Honsell, and Mitchell, and the Object Calculus of
	Abadi and Cardelli. Furthermore, the calculus allows us to get
	object oriented constructions unreachable in other calculi. In
	summa, we intend to show that because of its matching ability,
	the rho-calculus represents a ``lingua franca'' to naturally
	encode many paradigms of computations. This enlightens the
	capabilities of the rewriting calculus based language ELAN to
	be used as a logical as well as powerful semantical framework.
	}
}
@PHDTHESIS{CirsteaThese2000,
  author = {Cirstea,~Horatiu},
  title = {Calcul de r\'e\'ecriture~: fondements et applications},
  school = {Université Henri Poincaré - Nancy I},
  year = {2000},
  note = {October 25},
  pdf = {data/these.pdf},
  abstract = {L'objet de cette thèse est l'étude d'un calcul
	permettant de décrire l'application de règles de réécriture
	conditionnelles et de représenter les résultats obtenus. Nous
	introduisons le calcul de réécriture, appelé aussi le
	rho-calcul, qui généralise la réécriture du premier ordre et
	le lambda-calcul tout en permettant d'exprimer le
	non-déterminisme. Dans notre approche, l'opérateur
	d'abstraction ainsi que l'opérateur d'application sont des
	objets du calcul. Le résultat d'une réduction dans le calcul
	de réécriture est soit un ensemble vide représentant l'échec
	de l'application, soit un singleton représentant un résultat
	déterministe, soit un ensemble ayant plusieurs éléments
	représentant un choix non-déterministe de résultats.
	Au cours de cette thèse nous nous concentrons sur les
	propriétés du calcul de réécriture où le filtrage utilisé pour
	lier les variables à leurs valeurs actuelles est
	syntaxique. Nous définissons des stratégies d'évaluation
	garantissant la confluence du calcul et nous montrons que ces
	stratégies deviennent triviales pour des restrictions du
	calcul de réécriture général à des calculs plus simples comme
	le lambda-calcul. Le calcul de réécriture n'est pas terminant
	dans le cas non-typé mais la terminaison forte est obtenue en
	introduisant un typage des termes.
	Dans le calcul de réécriture étendu par un opérateur
	permettant de tester l'échec de l'application nous définissons
	des termes représentant la normalisation \textit{innermost} et
	\textit{outermost} par rapport à un ensemble de règles de
	réécriture. En utilisant ces termes, nous obtenons un codage
	naturel et concis de la réécriture conditionnelle. Enfin, à
	partir de la représentation des règles de réécriture
	conditionnelles, nous montrons comment le calcul de réécriture
	peut être employé pour donner une sémantique au langage {\sf ELAN},
	un langage basé sur l'application de règles de réécriture
	contrôlées par des stratégies.}
}
@INPROCEEDINGS{CirsteaKirchnerLiquoriRhoCube2001,
  author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi},
  title = {The {R}ho {C}ube},
  pages = {166-180},
  booktitle = {Foundations of Software Science and Computation Structures,
		     {http://www.disi.unige.it/etaps2001}{ETAPS'2001}},
  address = {Genova, Italy},
  editor = {Honsell, Furio},
  month = APR,
  publisher = {Springer-Verlag©},
  series = {{http://www.springer.de/comp/lncs/index.html}{Lecture Notes in Computer Science}},
  year = {2001},
  pdf = {data/fossacs2001.pdf},
  abstract = { The rewriting calculus, or Rho Calculus, is a
	simple calculus that uniformly integrates abstraction on
	patterns and non-determinism. Therefore, it fully integrates
	rewriting and Lambda-calculus. The original presentation of
	the calculus was "untyped".  In this paper we present a
	uniform way to decorate the terms of the calculus with types.
	This gives raise to a new presentation a la Church, together
	with nine (8+1) type systems which can be placed in a Rho-cube
	that extends the Lambda-cube of Barendregt. Due to the
	matching capabilities of the calculus, the type systems use
	only one abstraction mechanism and therefore gives an original
	answer to the identification of the standard "Lambda" and "Pi"
	abstractors.
 	As a consequence, this brings matching and rewriting as the
	first class concepts of the Rho-versions of the Logical
	Framework of Harper-Honsell-Plotkin, and of the Calculus of
	Constructions of Coquand-Huet.
	}
}
@ARTICLE{rhoCalIGLP-I-2001,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {The rewriting calculus --- {Part~I}},
  journal = {Logic Journal of the Interest Group in Pure and 
		   Applied Logics},
  year = {2001},
  volume = {9},
  number = {3},
  pages = {427--463},
  month = MAY,
  pdf = {data/iglp1.pdf},
  abstract = {The Rho-calculus integrates in a uniform and
	simple setting first-order rewriting, Lambda-calculus and
	non-deterministic computations.  Its abstraction mechanism is
	based on the rewrite rule formation and its main evaluation
	rule is based on matching modulo a theory T.
	In this first part, the calculus is motivated and its syntax
	and evaluation rules for any theory T are presented.  In the
	syntactic case, i.e. when T is the empty theory, we study its
	basic properties for the untyped case. We first show how it
	uniformly encodes Lambda-calculus as well as first-order
	rewriting derivations. Then we provide sufficient conditions
	for ensuring the confluence of the calculus.
	The rewriting calculus is a rule construction and application
	framework. As such it embeds in a uniform way term rewriting
	and Lambda-calculus. Since rule application is an explicit
	object of the calculus, it allows us also to handle the set of
	results explicitly.
	We present a simply typed version of the rewriting
	calculus. With a good choice of the type system, we show that
	the calculus is type preserving and terminating, i.e. verifies
	the subject reduction and strong normalization properties.
	}
}
@ARTICLE{rhoCalIGLP-II-2001,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {The rewriting calculus --- {Part~II}},
  journal = {Logic Journal of the Interest Group in Pure and 
		   Applied Logics},
  year = {2001},
  volume = {9},
  number = {3},
  pages = {465--498},
  month = MAY,
  pdf = {data/iglp2.pdf},
  abstract = {The Rho-calculus integrates in a uniform and
	simple setting first-order rewriting, Lambda-calculus and
	non-deterministic computations.  Its abstraction mechanism is
	based on the rewrite rule formation and its main evaluation
	rule is based on matching modulo a theory T.
	We have seen in the first part of this work the motivations,
	definitions and basic properties of the rho-calculus.  This
	second part is first devoted to the use of the rho-calculus
	for encoding a (conditional) rewrite relation. To this end we
	extend the calculus with a ``first'' operator whose purpose is
	to detect rule application failure. This extension allows us
	to express recursively rule application and therefore to
	encode strategy based rewriting processes. We then use this
	extended calculus to give an operational semantics to ELAN
	programs.
	We conclude with an overview of ongoing and future works on
	rho-calculus.
	}
}
@ARTICLE{rhoCalIGLP-I+II-2001,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {The rewriting calculus --- {Part~I {\em and} II}},
  journal = {Logic Journal of the Interest Group in Pure and Applied Logics},
  year = {2001},
  volume = {9},
  number = {3},
  pages = {427--498},
  month = MAY
}
@ARTICLE{BKKR-IJFCS-2001,
  author = {Borovansky,~Peter and Kirchner,~Claude and Ringeissen,~Christophe and Kirchner,~Helene},
  title = {Rewriting with strategies in {{\sf ELAN}}: 
		 a functional semantics},
  journal = {{International Journal of Foundations of Computer Science}},
  volume = {12},
  number = {1},
  pages = {69--98},
  month = FEB,
  year = {2001},
  pdf = {data/fuji.pdf},
  abstract = {In this work, we consider term rewriting from a
	functional point of view.  A rewrite rule is a function that
	can be applied to a term using an explicit application
	function. From this starting point, we show how to build more
	elaborated functions, describing first rewrite derivations,
	then sets of derivations.  These functions, that we call
	strategies, can themselves be defined by rewrite rules and the
	construction can be iterated leading to higher-order
	strategies.  Furthermore, the application function is itself
	defined using rewriting in the same spirit.  We present this
	calculus and study its properties. Its implementation in the
	ELAN language is used to motivate and exemplify the whole
	approach. The expressiveness of {\sf ELAN} is illustrated by
	examples of polymorphic functions and strategies.
	}
}
@INPROCEEDINGS{wmp2000,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {Rewriting and Multisets in the Rewriting Calculus and ELAN},
  booktitle = {{Workshop on Multiset Processing, Curtea de Arges, Romania}},
  year = {2000},
  month = { Aug},
  pdf = {data/wmp2000.pdf},
  abstract = {The rewriting calculus is a new calculus that integrates in a uniform and simple setting first-order rewriting, lambda-calculus and non-deterministic computations. The main design concept of the rewriting calculus is to make all the basic ingredients of rewriting explicit objects, in particular the notions of rule application and multisets of results. This paper describes the calculus from its syntax to its basic properties in the untyped case. The rewriting calculus embeds first-order conditional rewriting and lambda-calculus and it can be used in order to give an operational semantics to the rewrite based language Elan.  We show how the set-like data structures are easily represented in Elan and how this can be used in order to specify protocols.  }
}
@ARTICLE{multisetIST-I-2001,
  author = {Cirstea,~Horatiu and Kirchner,~Claude},
  title = {{R}ewriting and {M}ultisets in {R}ho-calculus and {{\sf ELAN}}},
  journal = {Romanian Journal of Information, Science and Technology},
  year = {2001},
  volume = {4},
  number = {1-2},
  pdf = {data/rjist.pdf},
  pages = {33--48},
  note = {ISSN: 1453-8245}
}
@INPROCEEDINGS{FaureKirchnerRhoException-RTA2002,
  author = {Faure,~Germain and Kirchner,~Claude},
  title = {Exceptions in the rewriting calculus},
  pages = {66--82},
  booktitle = {Proceedings of the RTA conference},
  volume = {2378},
  year = {2002},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  editor = {Tison, Sophie},
  address = {Copenhagen},
  month = JUL,
  pdf = {data/rhoException.pdf},
  abstract = {In the context of the rewriting calculus, we
	introduce and study an exception mechanism that allows us to
	express in a simple way rewriting strategies and that is
	therefore also useful for expressing theorem proving
	tactics. The proposed exception mechanism is expressed in a
	confluent calculus which gives the ability to simply express
	the semantics of the first tactical and to describe in full
	details the expression of conditional rewriting.}
}
@TECHREPORT{FaureMIM1-2001,
  author = {Faure,~Germain},
  title = {Etude des propri\'et\'es du calcul de réécriture: 
		  du rho au rho-epsilon calcul},
  institution = {LORIA et ENS Lyon},
  type = {Rapport du stage de première année du Magist\`ere 
		        d'Informatique et de Mod\'elisation de l'ENS Lyon},
  address = {Nancy},
  month = SEP,
  year = {2001},
  ps = {data/rhoGermain.pdf},
  abstract = {Abstract {html/rhoGermain-resume.html}{in French}, or 
		    {html/rhoGermain-abstract.html}{in English}}
}
@TECHREPORT{BenjaminDEA2002,
  author = {Wack,~Benjamin},
  title = {Aspects typés du calcul de réécriture},
  institution = {LORIA - ENS Lyon},
  year = {2002},
  type = {Rapport de DEA},
  address = {Nancy},
  month = JUL,
  pdf = {http://www.loria.fr/~wack/memoireDEA.pdf},
  abstract = {
Le calcul de réécriture, ou rho-calcul, intègre dans un même système le
lambda-calcul et la réécriture. Pour cela, les abstractions ne se font
plus seulement sur des variables mais sur des motifs. On profite ainsi à
la fois des mécanismes d'ordre supérieur du lambda-calcul et de
l'expressivité du filtrage de la réécriture. La complexité des divers
éléments du calcul font qu'il n'est pas confluent et donc qu'il faut
définir des stratégies, ou des restrictions, pour assurer la confluence.
Nous nous intéressons ici au rho-calcul en tant qu'extension du
lambda-calcul et nous en étudions les aspects typés. Notre étude se base
sur une généralisation du cube de Barendregt, où les deux abstracteurs
lambda et Pi sont unifiés en un seul. Il nous faut aussi tenir compte
des nouveaux éléments du rho-calcul : puissance du filtrage,
non-déterminisme, problèmes de confluence.
Sous les bonnes conditions, nous parvenons ainsi à prouver la plupart
des propriétés habituelles des calculs typés : lemme de substitution,
correction, préservation du type, consistance. Cependant, l'unicité du
type n'est généralement plus valable, notamment à cause de
l'unification des abstracteurs. Nous décrivons le nombre de
types distincts que peut avoir un terme donné, et nous montrons enfin
que l'unicité du typage reste valide dans les systèmes simplement typé
et polymorphe.
	}
}
@INPROCEEDINGS{HOR2002,
  author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi and Wack,~Benjamin},
  title = {The rewriting calculus : some results, some problems},
  booktitle = {The first international workshop on {H}igher-{O}rder
                  {R}ewriting},
  pages = {1 -- 2},
  year = {2002},
  editor = {Kesner, Delia and van Raamsdonk, Femke and Nipkow, Tobias},
  address = {Copenhagen, Denmark},
  month = JUL,
  organization = {FLoC'02},
  ps = {http://www.lri.fr/~kesner/hor/proc/proc.ps},
  abstract = {
The rewriting calculus, also called rho-calculus, embeds in a same
setting the lambda-calculus and the rewriting, by allowing abstraction
not only on variables but also on patterns.
The higher-order mechanisms of the lambda-calculus and the pattern
matching facilities of the rewriting are then both available at the
same level. It is worth noticing that the complexity of the calculus
breaks the confluence property, so that we need to define appropriate
strategies, or restrictions, in order to recover it.
We choose here to look at the rho-calculus as an extension of the
lambda-calculus, and we study the typed aspects. Our study is based upon
a generalization of Barendregt's lambda-cube, in which we unify both
abstractors lambda and Pi into a single one. We need to deal with the
original features of the rho-calculus too: matching power,
non-determinism, confluence issues.
With proper restrictions, we have proved most of the usual properties
for typed calculi: substitution lemma, correctness of types, subject
reduction, consistency. However, the uniqueness of typing is no longer
valid mainly because of the unification of both abstractors. We are
able to describe how many distinct types a term can admit and we can
still prove the uniqueness of typing for the two most restrictive
systems: simply typed and polymorphic.
	}
}
@TECHREPORT{ClaraDEA2002,
  author = {Bertolissi,~Clara},
  title = {dea},
  institution = {LORIA},
  year = {2002},
  type = {Rapport de DEA},
  address = {Nancy},
  month = JUL,
  abstract = {Dans ce rapport notre but est d'analyser la
  correspondance entre le calcul de réécriture et les relations de
  réécriture d'ordre supérieur. En particulier, nous montrons que pour
  toute réduction dans un CRS nous avons une réduction correspondante
  dans le calcul de réécriture et nous fournissons une traduction
  directe des CRS dans le calcul de réécriture.},
  ps = {data/deaClara.pdf}
}
@INPROCEEDINGS{RhoCal-Wrla2002,
  author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi},
  title = {Rewriting Calculus with(out) Types},
  booktitle = {Proceedings of the fourth workshop on rewriting logic 
		     and applications},
  year = {2002},
  editor = {Gadducci, Fabio and Montanari, Ugo},
  publisher = {Electronic Notes in Theoretical Computer Science},
  address = {Pisa (Italy)},
  month = SEP,
  comment = {Invited presentation by LL},
  pdf = {data/wrla2002.pdf},
  abstract = {The last few years have seen the development of a
	new calculus which can be considered as the outcome of the
	last decade of various researches on (higher order) term
	rewriting systems, and lambda calculi.  In the Rewriting
	Calculus (or Rho Calculus), algebraic rules are
	considered as sophisticated forms of ``lambda terms with
	patterns'', and rule applications as lambda applications with
	pattern matching facilities.
    
    	The calculus can be ``customized'' to work modulo
    	sophisticated algebraic theories, like commutativity,
    	associativity, associativity-commutativity, etc.  This allows
    	us to encode complex structures such as list, sets, and more
    	generally objects.  The calculus can be either be presented
    	``à la Curry'' or ``à la Church'' without sacrificing
    	readability and without complicating too much the metatheory.
    
    	The Rewriting Calculus could represent a \textit{lingua
    	franca} to encode many paradigms of computations together with
    	a formal basis used to build powerful theorem provers based on
    	lambda calculus and efficient rewriting, and a step towards
    	new proof engines based on the Curry-Howard isomorphism.
	}
}
@INPROCEEDINGS{ppts-popl2003,
  author = {Barthe,~Gilles and Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi},
  title = {Pure Patterns Type Systems},
  booktitle = {{ Principles of Programming Languages - POPL2003, New Orleans, USA}},
  year = 2003,
  month = JAN,
  publisher = {ACM},
  pdf = {data/popl2003.pdf},
  abstract = { We introduce a new framework of algebraic pure
	type systems in which we consider rewrite rules as lambda
	terms with patterns and rewrite rule application as
	abstraction application with built-in matching facilities.
	This framework, that we call \textit{``Pure Pattern Type
	Systems''}, is particularly well-suited for the foundations of
	programming (meta)languages and proof assistants since it
	provides in a fully unified setting higher-order capabilities
	and pattern matching ability together with powerful type
	systems.  We prove some standard properties like confluence
	and subject reduction for the case of a syntactic theory and
	under a syntactical restriction over the shape of patterns.
	We also conjecture the strong normalization of typable terms.
	This work should be seen as a contribution to a formal
	connection between logics and rewriting, and a step towards
	new proof engines based on the Curry-Howard isomorphism.}
}
@INPROCEEDINGS{rewritingStrategiesWRS2003,
  author = {Cirstea,~Horatiu and Kirchner,~Claude and Liquori,~Luigi and Wack,~Benjamin},
  title = {Rewrite Strategies in the Rewriting Calculus},
  booktitle = {{Proceedings of the Third International Workshop on Reduction Strategies 
                  in Rewriting and Programming }},
  year = 2003,
  month = JUN,
  publisher = {Electronic Notes in Theoretical Computer Science},
  editor = {Gramlich, Bernhard and Lucas, Salvador},
  pdf = {data/wrs2003.pdf},
  address = {Valencia, Spain},
  abstract = { This paper presents an overview on the use of the
	rewriting calculus to express rewrite strategies. We motivate
	first the use of rewrite strategies by examples in the elan\
	language. We then show how this has be modelled in the initial
	version of the rewriting calculus and how the matching power
	of this framework facilitates the writing of powerful
	strategies. }
}
@TECHREPORT{Faure03a,
  author = {Faure,~Germain},
  title = {Explicit Rewriting Calculus},
  year = { 2003},
  month = { Sep},
  institution = {ENS-Cachan,IRISA,LORIA},
  type = {Master Thesis},
  abstract = {The contributions of this report are twofold.
First, we will give the intuition  of how  programs can be represented
in the rewriting calculus. We will compare with the lambda-calculus and
take  many examples of OCaml programs.  Secondly,  we  propose,  study
and  exemplify  a  rewriting calculus with explicit constraint handling.
In this calculus, matching and application of   substitutions become
explicit. The approach is really modular, allowing extension to
arbitrary matching theories. We will also prove that the calculus is
powerful enough to deal with errors.  We will afterwards prove the
confluence of the calculus and the termination of the ``explicit'' part
of the calculus, some non trivial proofs. We conclude by an other
extension of the calculus to handle composition of substitutions. },
  ps = {data/reportdeaGF.pdf}
}
@TECHREPORT{CtreExKlop,
  author = {Wack, Benjamin},
  title = {Klop counter example in the Rho-Calculus},
  institution = {LORIA},
  year = {2003},
  type = {Draft notes},
  address = {Nancy},
  abstract = {We give a rho-translation of Klop's classical example about non-confluence for higher-order systems with non-linear matching.},
  ps = {data/spoofer.pdf}
}
@INPROCEEDINGS{BertolissiCirsteaKirchnerRULE03,
  author = {Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
  title = {{Translating Combinatory Reduction Systems into the 
Rewriting Calculus}},
  booktitle = {{Proceedings of the 4th International Workshop on 
Rule-Based Programming
Valencia, Spain, June 9, 2003}},
  year = 2003,
  month = JUN,
  publisher = {Electronic Notes in Theoretical Computer Science},
  editor = {Giavitto, Jean-Louis and Moreau, Pierre-Etienne},
  address = {Valencia, Spain},
  abstract = {The last few years have seen the development of the
    \emph{rewriting calculus} (or rho-calculus, RHO) that extends
    first order term rewriting and $\lambda$-calculus. The integration
    of these two latter formalisms has been already handled either by
    enriching first-order rewriting with higher-order capabilities,
    like in the \emph{Combinatory Reduction Systems}, or by adding to
    $\lambda$-calculus algebraic features. The different higher-order
    rewriting systems and the rewriting calculus share similar
    concepts and have similar applications, and thus, it seems natural
    to compare these formalisms.  We analyze in this paper the
    relationship between the Rewriting Calculus and the Combinatory
    Reduction Systems and we present a translation of
    CRS-terms and rewrite rules into rho-terms and we show
    that for any CRS-reduction we have a corresponding rho-reduction.},
  pdf = {data/rule03crsro.pdf}
}
@INPROCEEDINGS{CirsteaLiquoriWackTYPES03,
  author = {Cirstea,~Horatiu and Liquori,~Luigi and Wack,~Benjamin},
  title = {Rewriting Calculus with Fixpoints: Untyped and First-order Systems},
  year = {2003},
  volume = {3085},
  publisher = {Springer},
  pdf = {data/types2003.pdf},
  abstract = { The rewriting calculus, also called rho-calculus, is a framework embed
ding lambda-calculus and rewriting capabilities, by allowing abstraction not only on
variables but also on patterns. The higher-order mechanisms of the lambda-calculus and
the pattern matching facilities of the rewriting are then both available at the same
level. Many type systems for the lambda-calculus can be generalized to the rho-calculus:
in this paper, we study extensively a first-order rho-calculus \`a la Church, called
stk.
The type system of stk allows one to type (object oriented flavored) fixpoints,
leading to an expressive and safe calculus. In particular, using pattern matching,
one can encode and typecheck term rewriting systems in a natural and automatic
way. Therefore, we can see our framework as a starting point for the theoretical
basis of a powerful typed rewriting-based language.}
}
@INPROCEEDINGS{CirsteaFaureKirchnerWLRA2004,
  author = {Cirstea,~Horatiu and Faure,~Germain and Kirchner,~Claude},
  title = {A rho-calculus of explicit constraint application},
  booktitle = {Proceedings of the 5th workshop on rewriting logic
                     and applications},
  year = {2004},
  publisher = {vol. 117 of Electronic Notes in Theoretical Computer Science},
  pdf = {data/wrla2004-19.pdf},
  abstract = { Theoretical presentations of the rho-calculus often treat the
  matching constraint computations as an atomic operation although
  matching constraints are explicitly expressed. Actual implementations
  have to take a much more realistic view: computations needed in order
  to find the solutions of a matching equation can be really important
  in some matching theories and the substitution application usually
  involves a term traversal.
  Following the works on explicit substitutions in the
  \lambda-calculus, we propose, study and exemplify a rho-calculus with explicit constraint handling, up to the level of
  substitution applications. The approach is general, allowing the extension
  to various matching theories.
  We show that the calculus is powerful enough to deal with errors.
  We establish the confluence of the calculus and the termination of the
  explicit constraint handling and application sub-calculus.}
}
@INPROCEEDINGS{LiquoriWackWLRA2004,
  author = {Liquori,~Luigi and Wack,~Benjamin},
  title = {The Polymorphic Rewriting-calculus
[Type Checking vs. Type Inference]},
  booktitle = {Proceedings of the 5th workshop on rewriting logic
                     and applications},
  year = {2004},
  publisher = {vol. 117 of Electronic Notes in Theoretical Computer Science},
  pdf = {data/WRLA2004-13.pdf},
  abstract = { The Rewriting-calculus (Rho-calculus), is a minimal framework embedding Lambda-
calculus and Term Rewriting Systems, by allowing abstraction on variables and pat-
terns. The Rho-calculus features higher-order functions (from Lambda-calculus)
and pattern-matching (from Term Rewriting Systems). In this paper, we study
extensively a second-order Rho-calculus \`a la Church (RhoF) that enjoys subject
reduction, type uniqueness, and decidability of typing. We then apply a classi-
cal type-erasing function to RhoF obtaining an untyped Rho-calculus \`a la Curry
(uRhoF). The related type inference system is isomorphic to RhoF and enjoys sub-
ject reduction. Both RhoF and uRhoF systems can be considered as minimal calculi
for polymorphic rewriting-based programming languages. We discuss the possibility
of a logic existing underneath the type systems via a Curry-Howard Isomorphism.
}
}
@INPROCEEDINGS{WackTCS2004,
  author = {Wack,~Benjamin},
  title = {The simply-typed pure pattern type
system ensures strong normalization},
  year = 2004,
  publisher = {IFIP-WCC TCS},
  pdf = {data/rhoSN.pdf},
  abstract = {  Among the various type systems that have
been proposed, the type systems of the rho-cube are especially
interesting from a logical point of view, since they extend
Barendregt's rho-cube type systems. Strong normalization,
an essential property for logical soundness, had only been
conjectured so far: in this paper, we give a positive answer
for terms typed in the first-order system of the -cube.
The proof is based on a translation of terms and types
from the rewriting calculus into the rho-calculus. First, we
deal with untyped terms, ensuring that reductions are faith-
fully mimicked in the lambda-calculus. For this, we rely on an
original encoding of the pattern matching capability of the
rho-calculus into the lambda-calculus.
Then we show how to translate types: the expressive
power of System F is needed in order to fully reproduce
the original typing judgments of the rho-calculus. We prove
that the encoding is correct with respect to reductions and
typing, and we conclude with the strong normalization of
first-order typed rho-terms.}
}
@INPROCEEDINGS{LiquoriSerpettePPDP2004,
  author = {Liquori,~Luigi and Serpette,~Bernard},
  title = {i{R}ho, an imperative rewriting calculus},
  year = {2004},
  pdf = {data/iRho.pdf},
  publisher = {PPDP},
  abstract = { We propose an imperative version of the Rewriting-calculus, a calculus based on pattern-
matching, pattern-abstraction, and side-effects, which we call iRho.
We formulate a static and a call-by-value dynamic semantics of iRho like that of Gilles Kahn's Natural Semantics. The operational semantics is deterministic, and immediately suggests how to build an
interpreter for the calculus. The static semantics is given via a first-order type system based on a form
of product-type, which can be assigned to iRho-terms like structures (i.e. pairs).
The calculus is \`a la Church, i.e. pattern-abstractions are decorated with the types of the free variables
of the pattern.
iRho is a good candidate for a core or an intermediate language, because it can safely access and
modify a (monomorphic) typed store, and because fixed-points can be defined.
Properties like determinism of the interpreter, subject reduction, and decidability of type-checking
are completely checked by a machine assisted approach, using the Coq proof assistant. Progress and
decidability of type-checking are proved by pen and paper.}
}
@INPROCEEDINGS{rhoCalTermGraph2004,
  author = {Bertolissi,~Clara and Baldan,~Paolo and Cirstea,~Horatiu and Kirchner,~Claude},
  title = {{A} rewriting calculus for cyclic higher-order term graphs},
  year = {2004},
  pdf = {data/rhoGraphs.pdf},
  publisher = {Wokshop on term graph rewriting},
  abstract = {
Introduced at the end of the nineties, the Rewriting Calculus ($\rho$-calculus, for short)
is a simple calculus that fully integrates term-rewriting and -calculus. The rewrite
rules, acting as elaborated abstractions, their application and the obtained struc-
tured results are first class ob jects of the calculus. The evaluation mechanism,
generalizing beta-reduction, strongly relies on term matching in various theories.
   In this paper we propose an extension of the -calculus, handling graph like
structures rather than simple terms. The transformations are performed by explicit
application of rewrite rules as first class entities. The possibility of expressing
sharing and cycles allows one to represent and compute over regular infinite entities.
   The calculus over terms is naturally generalized by using unification constraints
in addition to the standard -calculus matching constraints. This therefore provides
us with the basics for a natural extension of an explicit substitution calculus to term
graphs. Several examples illustrating the introduced concepts are given.}
}
@ARTICLE{Wack06,
  author = {Wack,~Benjamin},
  title = {A {C}urry-{H}oward-{D}e {B}ruijn {I}somorphism {M}odulo},
  institution = {LORIA},
  year = {2006},
  address = {Nancy},
  journal = {Under submission},
  abstract = {   The rewriting calculus combines in a unified setting the
frameworks and capabilities of rewriting and lambda-calculus.
Its most general typed version, called Pure Pattern Type
Systems (PPTS) and adapted from Barendregt's lambda-cube, is
especially interesting from a logical point of view.
   We show how to use a subset of PPTS as a proof-
term language for natural deduction modulo, extending the
Curry-Howard-De Bruijn isomorphism for this class of log-
ical formalisms. The pattern matching featured in the cal-
culus allows us to model any congruence given by a term
rewriting system.
   We characterize how proofs can be denoted by PPTS
terms and we discuss the interest of our proof-term lan-
guage for the issue of cut elimination. Finally, we explore
some relations between our proof-term language and other
formalisms: extraction of lambda-terms and/or rewrite rules from
PPTS-terms, but also automated generation of proof-terms
by a rewriting-based language.},
  ps = {data/wack57.pdf}
}
@ARTICLE{HOSC05,
  author = {Cirstea,~Horatiu and Faure,~Germain and Kirchner,~Claude},
  title = {A Rho-Calculus of explicit constraint application},
  institution = {LORIA},
  year = {2005},
  address = {Nancy},
  journal = {To appear in  the journal of Higher-Order and Symbolic Computation},
  abstract = { 
 Theoretical presentations of the rho-calculus often treat the matching constraint computations as an
atomic operation although matching constraints are explicitly expressed. Actual implementations have to take a
much more realistic view: computations needed in order to find the solutions of a matching equation can have an
important impact on the (efficiency of the) calculus for some matching theories and the substitution application
usually involves a term traversal.
   Following the works on explicit substitutions in the -calculus, we present two versions of the rho-calculus, one
with explicit matching and one with explicit substitutions, together with a version that combines the two and
considers efficiency issues and more precisely the composition of substitutions. The approach is general, allowing
the extension to various matching theories. We establish the confluence of the calculus and the termination of
the explicit constraint handling and application sub-calculus.}
}
@PHDTHESIS{WackThese,
  author = {Wack,~Benjamin},
  title = {Typage et déduction dans le calcul de réécriture},
  school = {Université Henri Poincaré - Nancy I},
  year = {2005},
  optkey = {},
  type = {Thèse de doctorat},
  optaddress = {},
  month = OCT,
  pdf = {data/theseBenjamin.pdf},
  abstract = {The rewriting calculus is a formalism integrating functional
mechanisms from the lambda-calculus and matching capabilities from
rewriting. This thesis is devoted to the study of type systems for
this calculus, and to its applications to the domain of deduction.\\
We study the properties and the applications of two typing
paradigms. The first one is inspired by the simply typed
lambda-calculus, but it differs from it in the sense that even a
well-typed term may have a non-terminating reduction. Thus, we focus
on the use of this typed version for modeling programs, and especially
for representing rewriting systems.\\
The second family of type systems we study is adapted from the Pure
Type Systems, and features dependent types. We show the strong
normalization (which legitimates the use of the language in logic) in
two of these systems, via a translation into a lambda-calculus with
types depending on types.\\
Finally, we propose two ways of using the rewriting calculus in logic,
more particularly in relation with deduction modulo. In the first
approach, we use the systems with dependent types to define proof
terms for deduction modulo. In the second case, we define a generalization
of natural deduction and we show that a restricted form of matching is
useful in order to represent the rules of this deduction system.},
  optnote = {},
  optannote = {}
}
@PHDTHESIS{BertolissiThese,
  author = {Bertolissi,~Clara},
  title = {The graph rewriting calculus: properties and expressive capabilities},
  school = {Institut National Polytechnique Lorrain - INPL},
  year = {2005},
  optkey = {},
  type = {Thèse de doctorat},
  optaddress = {},
  month = OCT,
  pdf = {data/theseClara.pdf},
  abstract = { The last few years have seen the development of the rewriting calculus (also called rho-calculus) that uniformly integrates first-order term rewriting and lambda-calculus.
This thesis is devoted to the study of the expressiveness of the rewriting
calculus, with special interest for higher-order rewriting
and the possibility of dealing with graph-like structures.

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

The second part of the thesis is devoted to an extension of the rho-calculus,
called graph rewriting calculus (or  Rg-calculus), handling terms with sharing and cycles.
The calculus over terms is naturally generalised by using unification constraints in addition to standard rho-calculus matching constraints.
The Rg-calculus is shown to be confluent over equivalence classes of terms, under
some linearity restrictions on patterns, and expressive enough to simulate
first-order term graph rewriting and cyclic lambda-calculus. }
}
@ARTICLE{RgMSCS05,
  author = {Baldan,~Paolo and Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
  title = {A rewriting calculus for cyclic higher-order term graphs},
  institution = {Universit\'e de Venise and LORIA},
  year = {2005},
  address = {Nancy},
  journal = {To appear in  the journal of Mathematical Structures in Computer Science},
  abstract = { Introduced at the end of the nineties, the Rewriting Calculus
     (rho-calculus, for short) fully
     integrates term-rewriting and lambda-calculus.  The rewrite
     rules, acting as elaborated abstractions, their application and
     the obtained structured results are first class objects of the
     calculus.  The evaluation mechanism, generalising
     beta-reduction, strongly relies on term matching in various
     theories.
          In this paper we propose an extension of the rho-calculus,
     called Rg, handling structures with cycles and sharing rather
     than simple terms.      This is obtained by using unification constraints in addition to
     the standard rho-calculus matching constraints, which leads
     to a term-graph representation in an equational style.
     As for the classical RHO, the transformations are performed by
     explicit application of rewrite rules as first class entities.
     The possibility of expressing sharing and cycles allows one to
     represent and compute over regular infinite entities.
          We show that the (linear) Rg is confluent.  The proof of this
     result is quite elaborated, due to the non-termination of the
     system and to the fact that Rg-terms are considered modulo an
     equational theory.  We also show that the Rg is expressive
     enough to simulate first-order (equational) term-graph rewriting
     and lambda-calculus with explicit recursion (modelled using a letrec      like construct).
}
}
@ARTICLE{CrsHOSC04,
  author = {Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
  title = {Expressing Combinatory Reduction Systems Derivations in the Rewriting Calculus},
  institution = {LORIA},
  year = {2004},
  address = {Nancy},
  journal = {To appear in  the journal of Higher-Order and Symbolic Computation},
  abstract = { The last few years have seen the development of the
   rewriting calculus (also called rho-calculus or RHO) that
   uniformly integrates first-order term rewriting and
   lambda-calculus. The combination of these two latter formalisms
   has been already handled either by enriching first-order rewriting
   with higher-order capabilities, like in the Combinatory
   Reduction Systems (CRS), or by adding to lambda-calculus
   algebraic features. The various higher-order rewriting systems and
   the rewriting calculus share similar concepts and have similar
   applications, and thus, it is important to compare these
   formalisms to better understand their respective strengths and
   differences.

   We show in this paper that we can express Combinatory Reduction
   Systems derivations in terms of rewriting calculus
   derivations. The approach we present is based on a translation of
   each possible CRS-reduction into a corresponding
   rho-reduction. Since for this purpose we need to make precise
   the matching used when evaluating CRS, the second contribution of
   the paper is to present an original matching algorithm for CRS    terms that uses a simple term translation and the classical
   matching of lambda terms.
  }
}
@INPROCEEDINGS{bertolissi05a,
  crinnumber = {A05-R-413},
  category = {3},
  equipe = {PROTHEO},
  author = {Bertolissi,~Clara},
  title = {The graph rewriting calculus\,: confluence and expressiveness},
  booktitle = {{9th Italian conference on Italian Conference on Theoretical Computer Science - ICTCS 2005, Siena, Italy}},
  year = { 2005},
  editor = {Mario Coppo, Elena Lodi, G. Michele Pinna},
  volume = {3701},
  series = {Lecture Notes in Computer Science},
  pages = {113--127},
  month = { Oct},
  publisher = {Springer Verlag},
  pdf = {data/rhoGraph.pdf},
  abstract = {Introduced at the end of the nineties, the Rewriting Calculus (rho-calculus, for short) is a simple calculus that uniformly integrates term-rewriting and lambda-calculus. The Rhog has been recently introduced as an extension of the rho-calculus, handling structures with cycles and sharing. The calculus over terms is naturally generalized by using unification constraints in addition to the standard rho-calculus matching constraints. This leads to a term-graph representation in an equational style where terms consist of unordered lists of equations. In this paper we show that the (linear) Rhog is confluent. The proof of this result is quite elaborated, due to the non-termination of the system and to the fact that we work on equivalence classes of terms. We also show that the Rhog can be seen as a generalization of first-order term-graph rewriting, in the sense that for any term-graph rewrite step a corresponding sequence of rewritings can be found in the Rhog.}
}
@INPROCEEDINGS{FernandezM:intnrc,
  author = {Fernandez,~Maribel  and Mackie,~Ian and Sinot,~Francois-Regis},
  booktitle = {Proceedings of EXPRESS'05, satellite workshop of Concur},
  publisher = {Elsevier},
  series = {ENTCS},
  title = {Interaction Nets vs. the Rho-Calculus: Introducing Bigraphical Nets},
  year = {2005},
  pdf = {data/rhoIN.pdf},
  abstract = {
The rho-calculus generalises both term rewriting and the ¿-calculus in a uniform 
framework. Interaction nets are a form of graph rewriting which proved most suc- 
cessful in understanding the dynamics of the ¿-calculus, the prime example being the 
implementation of optimal  beta-reduction. It is thus natural to study interaction net 
encodings of the ¿-calculus as a first step towards the definition of efficient reduction 
strategies. We give two interaction net encodings which bring a new understanding 
to the operational semantics of the rho-calculus; however, these encodings have some 
drawbacks and to overcome them we introduce bigraphical nets--a new paradigm 
of computation inspired by Lafont's interactions nets and Milner's bigraphs. 

      }
}
@INPROCEEDINGS{CirFaurFerMacSin06,
  author = {Cirstea,~Horatiu and Faure,~Germain and Fernandez,~Maribel and Mackie,~Ian and Sinot,~Francois-Regis},
  booktitle = {Workshop on Reduction Strategies in Rewriting and Programming (WRS'06)},
  series = {ENTCS},
  title = { From Functional Programs to Interaction Nets via the Rewriting Calculus},
  year = {2006},
  pdf = {data/FPINrho.pdf},
  abstract = {We use the rho-calculus as an intermediate language to compile functional languages with pattern-matching 
features, and give an interaction net encoding of the rho-terms arising from the compilation. This encoding 
gives rise to new strategies of evaluation, where pattern-matching and traditional beta-reduction can proceed 
in parallel without overheads. 
}
}
@INPROCEEDINGS{BertolissiKirchner-fossacs2007,
  abstract = {The last few years have seen the development of the \emph{rewriting
                  calculus} (also called rho-calculus or \RHO) that uniformly integrates
                  first-order term rewriting and $\lambda$-calculus. The combination of
                  these two latter formalisms has been already handled either by enriching
                  first-order rewriting with higher-order capabilities, like in the
                  \emph{Combinatory Reduction Systems} (CRS), or by adding to
                  $\lambda$-calculus algebraic features.  

                  In a previous work, the authors
                  showed how the semantics of CRS can be expressed in terms of the
                  \RHO. The converse issue is adressed here: rewriting calculus
                  derivations are simulated by Combinatory Reduction Systems derivations.
                  As a consequence of this result, important properties, like
                  standardisation, are deduced for the rewriting calculus.  },
  address = {Braga, Portugal},
  author = {Bertolissi,~Clara and Kirchner,~Claude},
  booktitle = {Prooceedings the FoSSaCS},
  editor = {Seidl, Helmut},
  month = MAR,
  publisher = {Springer-Verlag},
  series = {LNCS},
  title = {The Rewriting Calculus as a Combinatory Reduction System},
  year = {2007},
  pdf = {data/bertolissiK-fossacs2007.pdf}
}
@ARTICLE{BALDAN:2006:INRIA-00110872:1,
  author = {Baldan,~Paolo and Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
  journal = {Mathematical Structures in Computer Science},
  title = {A rewriting calculus for cyclic higher-order term graphs},
  url = {https://hal.inria.fr/inria-00110872/en/},
  year = {2006},
  pdf = {data/rhoGraph-mscs.pdf},
  abstract = {Introduced at the end of the nineties, the Rewriting Calculus
                  (rho-calculus, for short) fully integrates term-rewriting and
                  lambda-calculus.  The rewrite rules, acting as elaborated abstractions,
                  their application and the obtained structured results are first class
                  objects of the calculus.  The evaluation mechanism, generalising
                  beta-reduction, strongly relies on term matching in various theories.
                  In this paper we propose an extension of the rho-calculus, called Rg,
                  handling structures with cycles and sharing rather than simple terms.
                  This is obtained by using unification constraints in addition to the
                  standard rho-calculus matching constraints, which leads to a term-graph
                  representation in an equational style.  As for the classical RHO, the
                  transformations are performed by explicit application of rewrite rules
                  as first class entities.  The possibility of expressing sharing and
                  cycles allows one to represent and compute over regular infinite
                  entities.  We show that the (linear) Rg is confluent.  The proof of this
                  result is quite elaborated, due to the non-termination of the system and
                  to the fact that Rg-terms are considered modulo an equational theory.
                  We also show that the Rg is expressive enough to simulate first-order
                  (equational) term-graph rewriting and lambda-calculus with explicit
                  recursion (modelled using a letrec like construct).  }
}
@ARTICLE{CIRSTEA:2006:INRIA-00110869:1,
  author = {Bertolissi,~Clara and Cirstea,~Horatiu and Kirchner,~Claude},
  journal = {Higher-Order and Symbolic Computation},
  title = {Expressing Combinatory Reduction Systems Derivations in the Rewriting Calculus},
  url = {https://hal.inria.fr/inria-00110869/en/},
  year = {2006},
  pdf = {data/CRS2Rho.pdf},
  abstract = { The last few years have seen the development of the rewriting
                  calculus (also called rho-calculus or RHO) that uniformly integrates
                  first-order term rewriting and lambda-calculus. The combination of these
                  two latter formalisms has been already handled either by enriching
                  first-order rewriting with higher-order capabilities, like in the
                  Combinatory Reduction Systems (CRS), or by adding to lambda-calculus
                  algebraic features. The various higher-order rewriting systems and the
                  rewriting calculus share similar concepts and have similar applications,
                  and thus, it is important to compare these formalisms to better
                  understand their respective strengths and differences.  We show in this
                  paper that we can express Combinatory Reduction Systems derivations in
                  terms of rewriting calculus derivations. The approach we present is
                  based on a translation of each possible CRS-reduction into a
                  corresponding rho-reduction. Since for this purpose we need to make
                  precise the matching used when evaluating CRS, the second contribution
                  of the paper is to present an original matching algorithm for CRS terms
                  that uses a simple term translation and the classical matching of lambda
                  terms.  }
}
@INPROCEEDINGS{CirsteaHoutmannWackWRLA2006,
  author = {Cirstea,~Horatiu and Houtmann,~Clement and Wack,~Benjamin},
  title = {Distributive Rho-Calculus},
  booktitle = {Sixth International Workshop on Reduction Strategies in
Rewriting and Programming},
  year = {2006},
  month = {Apr},
  address = {Vienna (Austria)},
  note = {accepted},
  pdf = {data/distrib-wrla2006.pdf},
  abstract = {
The rewriting calculus has been introduced as a general formalism that uniformly
integrates rewriting and  lambda-calculus. In this calculus all the basic ingredients of
rewriting such as rewrite rules, rule applications and results are first-class objects.
The rewriting calculus has been originally designed and used for expressing the
semantics of rule based as well as object oriented paradigms. We have previously
shown that convergent term rewriting systems and classic strategies can be encoded
naturally in the calculus.
In this paper, we go a step further and we propose an extended version of the
calculus that allows one to encode unrestricted term rewriting systems. This version
of the calculus features a new evaluation rule describing the behavior of the result
structures and a call-by-value evaluation strategy. We prove the confluence of the
obtained calculus and the correctness and completeness of the proposed encoding.
}
}
@INPROCEEDINGS{CirsteaF07,
  title = {Confluence of pattern-based lambda-calculi},
  author = {Horatiu Cirstea and Germain Faure},
  booktitle = {Rewriting Techniques and Applications},
  year = {2007},
  volume = {4533},
  pages = {78--92},
  pdf = {data/rta07.pdf},
  abstract = {
Different pattern calculi integrate the functional mechanisms from the
\lambda-calculus and the matching capabilities from rewriting. 
Several approaches are  used to obtain the confluence but  in practice the proof
methods share
the same structure and  each variation on the way
pattern-abstractions are applied needs another proof of confluence.

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

We show that our approach directly applies to different pattern
calculi, namely the lambda calculus with patterns, the pure pattern
calculus and the rewriting calculus.
We also characterize a class of matching algorithms and consequently
of pattern-calculi that are not confluent.
}
}
@INPROCEEDINGS{faureM07,
  title = {A Categorical Semantics of The Parallel Lambda-Calculus},
  author = {Germain Faure and Alexandre Miquel},
  year = {2007},
  volume = {Submited},
  pdf = {data/lics07.pdf},
  abstract = {In this paper, we define a sound and complete categorical semantics
  for the parallel lambda-calculus, based on a notion of
  aggregation monad which is modular w.r.t. associativity,
  commutativity and idempotence.

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

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

This file has been generated by bibtex2html 1.86.