@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -oc tmp/citePierre-Etienne.Moreau -ob tmp/Pierre-Etienne.Moreau.bib -c 'author:"Moreau, Pierre-Etienne"' biblio/complete.bib}}
@INPROCEEDINGS{moreau00a,
CRINNUMBER = {A00-R-398},
CATEGORY = {3},
EQUIPE = {PROTHEO},
AUTHOR = {Moreau, Pierre-Etienne},
TITLE = {REM (Reduce Elan Machine)\,: Core of the New ELAN Compiler},
BOOKTITLE = {{International Conference on Rewriting Techniques and Applications - RTA'2000, Norwich, UK}},
YEAR = {2000},
EDITOR = {Leo Bachmair},
VOLUME = {1833},
SERIES = {Lecture Notes in Computer Science},
PAGES = {265-269},
MONTH = {Jul},
ORGANIZATION = {Richard Kennaway},
PUBLISHER = {Springer-Verlag},
KEYWORDS = {rewriting, compilation, pattern matching},
ABSTRACT = {ELAN is a powerful language and environment for specifying and prototyping deduction systems in a language based on rewrite rules controlled by strategies. It offers a natural and simple logical framework for the combination of the computation and deduction paradigms. It supports the design of theorem provers, logic programming languages, constraint solvers and decision procedures. ELAN takes from functional programming the concept of abstract data types and the function evaluation principle based on rewriting. }
}
@MASTERSTHESIS{pierreetiennedea,
AUTHOR = {Moreau, Pierre-Etienne},
TITLE = {Compl\'etion avec contraintes en {ELAN}},
MONTH = {septembre},
SCHOOL = {{U}niversit\'e {H}enri {P}oincar\'e - {N}ancy 1},
TYPE = {{R}apport de {DEA}},
YEAR = {1994},
URL = {file://ftp.loria.fr/pub/loria/protheo/TECHNICAL_REPORTS_1994/PierreEtienneDEA.dvi.gz},
SUPPORT = {protheo}
}
@INPROCEEDINGS{kirchnerm-rta95,
AUTHOR = {Kirchner, Hélène and Moreau, Pierre-Etienne},
TITLE = {{Prototyping completion with constraints using
computational systems}},
BOOKTITLE = {Proceedings 6th Conference on Rewriting Techniques and
Applications},
EDITOR = {Hsiang, J.},
ADDRESS = {Kaiserslautern (Germany)},
PAGES = {438--443},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {914},
YEAR = {1995},
URL = {file://ftp.loria.fr/pub/loria/protheo/COMMUNICATIONS_1995/KirchnerM-RTA95.dvi.gz},
SUPPORT = {protheo,ccl}
}
@INPROCEEDINGS{elan-rwlg1996,
AUTHOR = {Borovansky, Peter and Kirchner, Claude and Kirchner, Hélène and
Moreau, Pierre-Etienne and Vittek, Marian},
TITLE = {{ELAN: A logical framework based on computational
systems}},
BOOKTITLE = {Proceedings of 1st International Workshop on Rewriting
Logic},
EDITOR = {Meseguer, J.},
ADDRESS = {Asilomar (CA, USA)},
MONTH = {September},
PUBLISHER = {Electronic Notes in Theoretical Computer Science},
VOLUME = {4},
YEAR = {1996},
URL = {file://ftp.loria.fr/pub/loria/protheo/COMMUNICATIONS_1996/elan-rwlg1996.ps.gz},
SUPPORT = {protheo}
}
@INPROCEEDINGS{reflection-rwlg1996,
AUTHOR = {Kirchner, Hélène and Moreau, Pierre-Etienne},
TITLE = {{A reflective extension of ELAN}},
BOOKTITLE = {Proceedings of 1st International Workshop on Rewriting
Logic},
EDITOR = {Meseguer, J},
ADDRESS = {Asilomar (CA, USA)},
MONTH = {September},
PUBLISHER = {Electronic Notes in Theoretical Computer Science},
VOLUME = {4},
YEAR = {1996},
URL = {file://ftp.loria.fr/pub/loria/protheo/COMMUNICATIONS_1996/Reflection-RwLg1996.ps.gz},
SUPPORT = {protheo}
}
@INPROCEEDINGS{moreauk-asf+sdf97,
AUTHOR = {Moreau, Pierre-Etienne and Kirchner, Hélène},
TITLE = {{Compilation Techniques for Associative-Commutative
Normalisation}},
BOOKTITLE = {Proceedings of International Workshop on Theory and
Practice of Algebraic Specifications ASF+SDF 97},
ADDRESS = {Amsterdam (The Netherlands)},
MONTH = {September},
PUBLISHER = {Springer-Verlag},
SERIES = {Workshops in Computing},
YEAR = {1997},
URL = {file://ftp.loria.fr/pub/loria/protheo/COMMUNICATIONS_1997/MoreauK-ASFSDF97.ps.gz},
SUPPORT = {protheo}
}
@TECHREPORT{moreauk-crin97,
AUTHOR = {Moreau, Pierre-Etienne and Kirchner, Hélène},
TITLE = {{Compilation of Associative-Commutative Normalisation with
Strategies in ELAN (Full version)}},
INSTITUTION = {LORIA},
ADDRESS = {Nancy (France)},
NUMBER = {97-R-129},
TYPE = {Technical Report},
YEAR = {1997},
URL = {file://ftp.loria.fr/pub/loria/protheo/TECHNICAL_REPORTS_1997/MoreauK-97-R-129.ps.gz},
SUPPORT = {protheo}
}
@INPROCEEDINGS{borovansky98e,
AUTHOR = {Borovansky, Peter and Jamoussi, S. and Moreau, Pierre-Etienne and
Ringeissen, Christophe},
TITLE = {{Handling ELAN Rewrite Programs via an Exchange Format}},
BOOKTITLE = {Second Workshop on Rewriting Logic and its Applications -
WRLA'98},
EDITOR = {Kirchner, Claude and Kirchner, Hélène},
ADDRESS = {Pont-\`a-Moussson (France)},
PUBLISHER = {Elsevier Science B. V.},
SERIES = {Electronic Notes in Theoretical Computer Science},
VOLUME = {15},
YEAR = {1998},
URL = {file://ftp.loria.fr/pub/loria/protheo/COMMUNICATIONS_1998/BorovanskyJMR-WRLA98.ps.gz},
SUPPORT = {protheo}
}
@INPROCEEDINGS{borovansky98f,
AUTHOR = {Borovansky, Peter and Kirchner, Claude and Kirchner, Hélène and
Moreau, Pierre-Etienne and Ringeissen, Christophe},
TITLE = {{An Overview of ELAN}},
BOOKTITLE = {Second Workshop on Rewriting Logic and its Applications
WRLA'98},
EDITOR = {Kirchner, Claude and Kirchner, Hélène},
ADDRESS = {Pont-\`a-Mousson (France)},
PUBLISHER = {Elsevier Science B. V.},
SERIES = {Electronic Notes in Theoretical Computer Science},
VOLUME = {15},
YEAR = {1998},
NOTE = {URL: http://www.elsevier.nl/locate/entcs/volume15.html},
URL = {file://ftp.loria.fr/pub/loria/protheo/COMMUNICATIONS_1998/BorovanskyKKMR-WRLA98.ps.gz},
SUPPORT = {protheo}
}
@INPROCEEDINGS{kirchner98e,
AUTHOR = {Kirchner, Hélène and Moreau, Pierre-Etienne},
TITLE = {{Non-deterministic computations in ELAN}},
BOOKTITLE = {Proceedings of 13th International Workshop on Recent
Developments in Algebraic Development Techniques
(WADT'98)},
EDITOR = {Fiadeiro, J. L.},
ADDRESS = {Lisbon (Portugal)},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
YEAR = {1998},
NOTE = {Selected Paper},
SUPPORT = {protheo}
}
@INPROCEEDINGS{moreau-jicslpw98,
AUTHOR = {Moreau, Pierre-Etienne},
TITLE = {{A choice-point library for backtrack programming}},
BOOKTITLE = {Proceedings of JICSLP'98 Post-Conference Workshop on
Implementation Technologies for Programming Languages based
on Logic},
EDITOR = {Sagolas, K.},
ADDRESS = {Manchester (UK)},
PAGES = {16--31},
YEAR = {1998},
URL = {file://ftp.loria.fr/pub/loria/protheo/COMMUNICATIONS_1998/Moreau-JICSLP98.ps.gz},
SUPPORT = {protheo,ccl}
}
@TECHREPORT{moreau98a,
AUTHOR = {Moreau, Pierre-Etienne},
TITLE = {{Compiling nondeterministic computations}},
INSTITUTION = {LORIA},
ADDRESS = {Nancy (France)},
NUMBER = {98-R-005},
TYPE = {Technical Report},
YEAR = {1998},
URL = {file://ftp.loria.fr/pub/loria/protheo/TECHNICAL_REPORTS_1998/Moreau-98-R-005.ps.gz},
SUPPORT = {protheo}
}
@INPROCEEDINGS{moreau98b,
AUTHOR = {Moreau, Pierre-Etienne and Kirchner, Hélène},
TITLE = {{A Compiler for Rewrite Programs in
Associative-Commutative Theories}},
BOOKTITLE = {ALP/PLILP: Principles of Declarative Programming},
EDITOR = {Palamidessi, C. and Glaser, H. and Meinke, K.},
ADDRESS = {Pisa (Italy)},
MONTH = {September},
PAGES = {230-249},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1490},
YEAR = {1998},
URL = {file://ftp.loria.fr/pub/loria/protheo/COMMUNICATIONS_1998/MoreauK-PLILP98.ps.gz},
SUPPORT = {protheo,ccl}
}
@TECHREPORT{borovansky99b,
AUTHOR = {Borovansky, Peter and Kirchner, Claude and Kirchner,
Hélène and Moreau, Pierre-Etienne},
TITLE = {{ELAN from the rewriting logic point of view}},
INSTITUTION = {LORIA},
ADDRESS = {Nancy (France)},
MONTH = {November},
NUMBER = {99-R-284},
TYPE = {Technical Report},
YEAR = {1999},
SUPPORT = {protheo}
}
@PHDTHESIS{moreau99a,
AUTHOR = {Moreau, Pierre-Etienne},
TITLE = {{Compilation de règles de réécriture et de
stratégies non-déterministes}},
MONTH = {June},
SCHOOL = {Universit\'e Henri Poincar\'e -- Nancy 1},
TYPE = {Thèse de Doctorat d'Université},
YEAR = {1999},
NOTE = {Also available as Technical Report 99-T-083, LORIA, Nancy
(France)},
URL = {file://ftp.loria.fr/pub/loria/protheo/THESES_1999/Moreau-These99.ps.gz},
SUPPORT = {protheo,ccl}
}
@ARTICLE{kirchner01a,
AUTHOR = {Kirchner, Hélène and Moreau, Pierre-Etienne},
TITLE = {{Promoting Rewriting to a Programming Language: A Compiler
for Non-Deterministic Rewrite Programs in
Associative-Commutative Theories}},
JOURNAL = {Journal of Functional Programming (JFP)},
MONTH = {March},
NUMBER = {2},
PAGES = {207-251},
VOLUME = {11},
YEAR = {2001},
NOTE = {Also available as Technical Report A01-R-007, LORIA, Nancy
(France)},
SUPPORT = {protheo,ccl}
}
@INPROCEEDINGS{moreau01a,
AUTHOR = {Moreau, Pierre-Etienne and Ringeissen, Christophe and Vittek, Marian},
TITLE = {{A Pattern-Matching Compiler}},
BOOKTITLE = {{First Workshop on Language Descriptions, Tools and
Applications (LDTA'01)}},
EDITOR = {van den Brand, M. and Parigot, D.},
ADDRESS = {Genova (Italy)},
MONTH = {April},
PUBLISHER = {Elsevier},
SERIES = {Electronic Notes in Theoretical Computer Science},
VOLUME = {44-2},
YEAR = {2001},
NOTE = {Also available as Technical Report A01-R-059, LORIA, Nancy
(France)},
SUPPORT = {protheo}
}
@ARTICLE{borovansky02a,
CRINNUMBER = {A02-R-441},
CATEGORY = {1},
EQUIPE = {PROTHEO},
AUTHOR = {Borovansky, Peter and Kirchner, Claude and Kirchner, Hélène and Moreau, Pierre-Etienne},
TITLE = {{ELAN from a rewriting logic point of view}},
JOURNAL = {Theoretical Computer Science},
YEAR = 2002,
NUMBER = {285},
PAGES = {155-185},
MONTH = JUL
}
@TECHREPORT{moreau02b,
CRINNUMBER = {A02-R-184},
CATEGORY = {15},
EQUIPE = {PROTHEO},
AUTHOR = {Moreau, Pierre-Etienne and Ringeissen, Christophe and Vittek, Marian},
TITLE = {{A Pattern Matching Compiler for Multiple Target Languages}},
YEAR = 2002,
TYPE = {Rapport de recherche},
MONTH = OCT,
URL = {http://www.loria.fr/publications/2002/A02-R-184/A02-R-184.ps}
}
@TECHREPORT{moreau02a,
CRINNUMBER = {A02-R-126},
CATEGORY = {15},
EQUIPE = {PROTHEO},
AUTHOR = {Moreau, Pierre-Etienne and Zendra, Olivier},
TITLE = {{GC?\,: A Generational Conservative Garbage Collector for the ATerm Library}},
YEAR = 2002,
TYPE = {Rapport de recherche},
MONTH = SEP,
URL = {http://www.loria.fr/publications/2002/A02-R-126/A02-R-126.ps}
}
@INPROCEEDINGS{van_den_brand02a,
CRINNUMBER = {A02-R-525},
CATEGORY = {3},
EQUIPE = {PROTHEO},
AUTHOR = {van den Brand, Mark G. J. and Moreau, Pierre-Etienne and Ringeissen, Christophe},
TITLE = {{The ELAN Environment\,: an Rewriting Logic Environment based on ASF+SDF Technology}},
BOOKTITLE = {{Workshop on Language Descriptions, Tools and Applications - LDTA'02, Grenoble, France}},
YEAR = 2002,
VOLUME = {65},
NUMBER = {3},
SERIES = {Electronic Notes in Theoretical Computer Science},
MONTH = APR
}
@INPROCEEDINGS{cridlig03b,
CRINNUMBER = {A03-R-205},
CATEGORY = {3},
EQUIPE = {MADYNES},
AUTHOR = {Cridlig, Vincent and Festor, Olivier and Guyard, Jacques and Moreau, Pierre-Etienne},
TITLE = {Formalisation et évaluation de politiques P3P},
BOOKTITLE = {{Colloque Francophone sur l'Ingénierie des Protocoles 2003 CFIP2003}},
YEAR = {2003},
MONTH = {Oct},
KEYWORDS = {policy, rewriting rules, p3p, appel, elan},
ABSTRACT = {L'écriture et l'évaluation de politiques est un problème qui revient de fa\c{c}on récurrente dans l'internet. Ces politiques, qui touchent des domaines comme la confidentialité(P3P), la sécurité (firewall) ou le provisionning (COPS-PR) sont très souvent composées d'un certain nombre de règles {\`a} parcourir suivant un ordre déterminé. Dans cet article, nous présentons les résultats de nos travaux sur la formalisation des règles P3P et leur validation dans un environnement formel basé sur la réécriture. Nous réalisons notamment un environnement qui, {\`a} partir d'une politique P3P et de préférences utilisateurs en langage APPEL, retourne le comportement {\`a} adopter vis {\`a} vis d'une ressource sur Internet. Ce prototype utilise le langage ELAN.}
}
@INPROCEEDINGS{cridlig03c,
CRINNUMBER = {A03-R-206},
CATEGORY = {3},
EQUIPE = {MADYNES},
AUTHOR = {Cridlig, Vincent and Festor, Olivier and Guyard, Jacques and Moreau, Pierre-Etienne},
TITLE = {A Formal Approach to P3P Privacy Policies Evaluation},
BOOKTITLE = {{9th Open European Summer School and IFIP Workshop on Next Generation Networks - EUNICE 2003, hungary, Budapest}},
YEAR = {2003},
MONTH = {Sep},
KEYWORDS = {policy, rewriting rules, p3p, appel, elan},
ABSTRACT = {Writing and evaluating policies is a recurrent problem over the Internet. These policies, which deal with fields like privacy (P3P), security (P3P) and provisioning (COPS-PR) are often made of many ordered rules. In this paper, we present our work related to P3P rules formalization and validation in an evaluation environnement based on rewriting process. We also develop an environnement which returns the right behavior regarding Internet ressources, P3P policies and APPEL user's preferences.}
}
@INPROCEEDINGS{moreau03a,
CRINNUMBER = {A03-R-357},
CATEGORY = {3},
EQUIPE = {PROTHEO},
AUTHOR = {Moreau, Pierre-Etienne and Ringeissen, Christophe and Vittek, Marian},
TITLE = {A Pattern Matching Compiler for Multiple Target Languages},
BOOKTITLE = {{International Conference on Compiler Construction - CC'2003, Varsovie, Pologne}},
YEAR = {2003},
EDITOR = {Görel Hedin},
VOLUME = {2622},
SERIES = {Lecture notes in Computer Science},
PAGES = {61-76},
MONTH = {Apr},
KEYWORDS = {compilation, pattern matching, rewriting},
ABSTRACT = {Many processes can be seen as transformations of tree-like data structures. In compiler construction, for example, we continuously manipulate trees and perform tree transformations. This paper introduces a pattern matching compiler (TOM)\,: a set of primitives which add pattern matching facilities to imperative languages such as C, Java, or Eiffel. We show that this tool is extremely non-intrusive, lightweight and useful to implement tree transformations. It is also flexible enough to allow the reuse of existing data structures. }
}
@INPROCEEDINGS{van_den_brand03a,
CRINNUMBER = {A03-R-438},
CATEGORY = {3},
EQUIPE = {GLT},
AUTHOR = {van den Brand, Mark and Moreau, Pierre-Etienne and Vinju, Jurgen},
TITLE = {Environments for Term Rewriting Engines for Free!},
BOOKTITLE = {{International Conference on Rewriting Techniques and Applications - RTA'2003, Valence, Espagne}},
YEAR = {2003},
EDITOR = {Robert Nieuwenhuis},
VOLUME = {2706},
SERIES = {Lecture notes in Computer Science},
PAGES = {424-435},
MONTH = {Jun},
PUBLISHER = {Springer},
KEYWORDS = {rewriting, environment},
ABSTRACT = {Term rewriting can only be applied if practical implementations of term rewriting engines exist. New rewriting engines are designed and implemented either to experiment with new (theoretical) results or to be able to tackle new application areas. In this paper we present the Meta-Environment\,: an environment for rapidly implementing the syntax and semantics of term rewriting based formalisms. We provide not only the basic building blocks, but complete interactive programming environments that only need to be instantiated by the details of a new formalism. }
}
@ARTICLE{moreau04a,
CRINNUMBER = {A04-R-146},
CATEGORY = {1},
EQUIPE = {PROTHEO},
AUTHOR = {Moreau, Pierre-Etienne and Zendra, Olivier},
TITLE = {GC$^2$\,: A Generational Conservative Garbage Collector for the ATerm Library},
JOURNAL = {The Journal of Logic and Algebraic Programming (JLAP)},
YEAR = {2004},
VOLUME = {59},
NUMBER = {1-2},
PAGES = {5-34},
MONTH = {Apr},
KEYWORDS = {aterms, hash-consing, memory management, garbage collection, generations, mark-and-sweep},
ABSTRACT = {The ATerm library is a well-designed and well-known library in the term rewriting community. In this paper, we discuss the current garbage collector provided with the library and stress the fact that some peculiarities of this functional library could be taken advantage of by the memory management system. We explain how we designed and implemented GC$^2$, a new mark-and-sweep generational garbage collector for the ATerm library that builds upon these peculiarities. Experimental results on various programs validate our approach, and show that the performance of our new algorithm is very good. }
}
@INPROCEEDINGS{cirstea04a,
CRINNUMBER = {A04-R-256},
CATEGORY = {3},
EQUIPE = {PROTHEO},
AUTHOR = {Cirstea, Horatiu and Moreau, Pierre-Etienne and Reilles, Antoine},
TITLE = {Rule based programming in Java for protocol verification},
BOOKTITLE = {{5th International Workshop on Rewriting Logic and its Applications - WRLA'2004, Barcelona, Spain}},
YEAR = {2004},
EDITOR = {Narciso Marti-Oliet and Manuel Clavel and Alberto Verdejo},
SERIES = {Electronic Notes in Theoretical Computer Science},
MONTH = {Mar},
ORGANIZATION = {Narciso Marti-Oliet},
PUBLISHER = {Elsevier},
KEYWORDS = {model-checking, rewriting},
ABSTRACT = {This paper presents an approach for the development of model-checkers in a framework, called Tom, merging declarative and imperative features. We illustrate our method by specifying in Tom the Needham-Schroeder Public-Key protocol that aims to establish a mutual authentication between an initiator and a responder that communicate via an insecure network. We describe the behavior of the agents exchanging messages as well as the intruders and the security invariants the protocol should verify using the rewrite rules of Tom. The (depth-first or breadth-first) exploration of the search space is described using the imperative features of the language. We propose several optimizations and we compare our results to existing approaches.}
}
@INPROCEEDINGS{guyon04a,
CRINNUMBER = {A04-R-257},
CATEGORY = {3},
EQUIPE = {PROTHEO},
AUTHOR = {Guyon, Julien and Moreau, Pierre-Etienne and Reilles, Antoine},
TITLE = {An Integrated Development Environment for Pattern Matching Programming},
BOOKTITLE = {{2nd eclipse Technology eXchange workshop - eTX'2004, Barcelona, Spain}},
YEAR = {2004},
SERIES = {Electronic Notes in Theoretical Computer Science},
MONTH = {Apr},
ORGANIZATION = {Brian Barry and Oege de Moor},
KEYWORDS = {eclipse, pattern matching, java},
ABSTRACT = {Tom and Apigen are two complementary tools which simplify the definition and the manipulation of abstract datatypes. Tom is an extension of Java which adds pattern matching facilities independently of the used data-structure. Apigen is a generator of abstract syntax tree implementations which interacts naturally with \tom. In this paper, we show how Eclipse can be extended to support the development of Tom programs. By integrating a Tom editor, an automatic build process, and an error management mechanism, we demonstrate the integration of an algebraic programming environment in Eclipse. Hence, our work contributes to the promotion of formal methods and Eclipse to the educational, algebraic, and industrial communities. }
}
@ARTICLE{van_den_brand04a,
CRINNUMBER = {A04-R-258},
CATEGORY = {1},
EQUIPE = {SEN},
AUTHOR = {van den Brand, Mark and Moreau, Pierre-Etienne and Vinju, Jurgen},
TITLE = {A generator of efficient strongly typed abstract syntax trees in Java},
JOURNAL = {IEE Proceedings - Software Engineering},
YEAR = {2004},
MONTH = {Dec},
KEYWORDS = {abstract data-type, maximal sharing, java, generator},
ABSTRACT = {Abstract syntax trees are a very common data-structure in language related tools. For example compilers, interpreters, documentation generators, and syntax-directed editors use them extensively to extract, transform, store and produce information that is key to their functionality. We present a Java back-end for Apigen, a tool that generates implementations of abstract syntax trees. The generated code is characterized by strong typing combined with a generic interface and maximal sub-term sharing for memory efficiency and fast equality checking. The goal of this tool is to obtain safe and more efficient programming interfaces for abstract syntax trees. The contribution of this work is the combination of generating a strongly typed data-structure with maximal sub-term sharing in Java. Practical experience shows that this approach is beneficial for extremely large as well as smaller data types.}
}
@TECHREPORT{cirstea04f,
CRINNUMBER = {A04-R-563},
CATEGORY = {13},
EQUIPE = {PROTHEO},
AUTHOR = {Cirstea, Horatiu and Kirchner, Claude and Moossen, Michael and Moreau, Pierre-Etienne},
TITLE = {Production Systems and Rewrite Systems},
YEAR = {2004},
TYPE = {Rapport Intermédiaire},
MONTH = {Nov},
URL = {http://www.loria.fr/publications/2004/A04-R-563/A04-R-563.ps},
KEYWORDS = {term rewriting, business rule, production rules, associative-commutative matching, matching constraint},
ABSTRACT = {This report studies the relationship between systems and term rewrite systems. Giving a
brief definition of both, then comparing all the concepts related to them, their similarities
and differences, comparing also the life cycle of each system for finally to study ways for
translating one to another. }
}
@TECHREPORT{cirstea04d,
CRINNUMBER = {A04-R-546},
CATEGORY = {13},
EQUIPE = {PROTHEO},
AUTHOR = {Cirstea, Horatiu and Kirchner, Claude and Moossen, Michael and Moreau, Pierre-Etienne},
TITLE = {Production Systems and Rete Algorithm Formalisation},
YEAR = {2004},
TYPE = {Rapport Intermédiaire},
MONTH = {Oct},
URL = {http://www.loria.fr/publications/2004/A04-R-546/A04-R-546.ps},
KEYWORDS = {term rewriting, business rule, production rules, rete network, matching},
ABSTRACT = {The rete algorithm is a well-known algorithm for efficiently addressing the many patterns/many objects match problem, and it has been widely used and implemented in several applications, mainly production systems. But despite of the wide usage of production systems and the rete algorithm, to the best of our knowledge there has been just one proposition for a formal definition of the rete algorithm given by Fages and Lissajoux~\cite{Fages92}, but no attempt to give a formal description of production systems as a whole, giving rise to lots of ambiguities and incompatibilities between the different implementations. Therefore, the need for a formalisation is clear and we present in this report a first approach to it, refining Fages and Lissajoux's approach to fit it in our general model of production systems.}
}
@TECHREPORT{kirchner05a,
CRINNUMBER = {A05-R-005},
CATEGORY = {15},
EQUIPE = {PROTHEO},
AUTHOR = {Kirchner, Claude and Moreau, Pierre-Etienne and Reilles, Antoine},
TITLE = {Formal Validation of Pattern Matching Code},
YEAR = {2005},
TYPE = {Rapport de recherche},
MONTH = {Jan},
KEYWORDS = {compilation, pattern matching, multi-match, term rewriting, verified code},
ABSTRACT = {When addressing the problem of software formal validation, two main alternatives consist either to prove the correctness of compilers or to directly validate the generated code. We address here the specific problem of directly proving the correctness of compiled code issued from powerful pattern matching constructions appearing in high-level programming languages as ML like languages or rewrite based languages such as ELAN or Tom. In this context, our first contribution is to define a general framework allowing to anchor algebraic pattern-matching capabilities in existing languages like C, Java or ML. Then, using a just enough powerful intermediate language, we formalize the behavior of compiled code and define the correctness of compiled code with respect to pattern-matching behavior. This allows us to prove the equivalence of compiled code correctness with a generic first-order proposition whose proof could be achieved via a proof assistant or an automated theorem prover. We then extend these results to the multi-match situation characteristic of the ML like languages. The whole approach has been implemented on top of the Tom compiler and used to validate the syntactic matching code of the Tom compiler itself.}
}
@ARTICLE{VANDENBRAND:2005:43624,
TITLE = {Generator of efficient strongly typed abstract syntax trees in Java },
AUTHOR = {Van Den Brand, Mark and Moreau, Pierre-Etienne and Vinju, Jurgen},
ABSTRACT = {Abstract syntax trees are a very common data-structure in language related tools. For example compilers, interpreters, documentation generators, and syntax-directed editors use them extensively to extract, transform, store and produce information that is key to their functionality. We present a Java back-end for ApiGen, a tool that generates implementations of abstract syntax trees. The generated code is characterized by strong typing combined with a generic interface and maximal sub-term sharing for memory efficiency and fast equality checking. The goal of this tool is to obtain safe and more efficient programming interfaces for abstract syntax trees. The contribution of this work is the combination of generating a strongly typed data-structure with maximal sub-term sharing in Java. Practical experience shows that this approach is beneficial for extremely large as well as smaller data types. },
LANGUAGE = {Anglais },
AFFILIATION = {PROTHEO [INRIA Lorraine - LORIA] - Centrum voor Wiskunde en Informatica [CWI] },
BOOKTITLE = {IEE Proceedings - Software Engineering },
PUBLISHER = {IEEE },
PAGES = {70--87 70--87 },
JOURNAL = {IEE Proceedings - Software Engineering },
TYPE = {Avec comit\'{e} de lecture },
VOLUME = {152 },
NUMBER = {2 },
NOTE = {publi\'{e} },
ISSN = {1364-5080},
DAY = {01},
MONTH = {04},
YEAR = {2005},
URL = {http://hal.inria.fr/inria-00000700/en/}
}
@INPROCEEDINGS{BALLAND:2005:44109,
TITLE = {Optimizing Pattern Matching by Program Transformation },
AUTHOR = {Balland, Emilie and Moreau, Pierre-Etienne},
ABSTRACT = {In this paper we present a new compilation method based on program transformation. The principle is to separate the compilation of pattern matching from its optimization, and describe optimizations using transformation rules. This eases the compilation of extensions, such as new equational theories, or the addition of or-patterns for example. In addition, we show that the proposed optimizations are correct and effective in practice. The presented approach has been implemented and applied to Tom, a language extension which adds pattern-matching facilities to C and Java. },
LANGUAGE = {Anglais },
AFFILIATION = {PROTHEO [INRIA Lorraine - LORIA] },
BOOKTITLE = {Compilation Construction (CC) Compilation Construction (CC) },
ADDRESS = {Vienne, Autriche },
TYPE = {Avec comit\'{e} de lecture },
NOTE = {en cours de soumission Non },
DAY = {14},
MONTH = {10},
YEAR = {2005},
URL = {http://hal.inria.fr/inria-00000763/en/}
}
@INPROCEEDINGS{KAHRAMANOGULLARI:2005:43622,
TITLE = {Implementing Deep Inference in Tom },
AUTHOR = {Kahramanogullari, Ozan and Moreau, Pierre-Etienne and Reilles, Antoine},
ABSTRACT = {The calculus of structures is a proof theoretical formalism which generalizes sequent calculus with the feature of deep inference: in contrast to sequent calculus, the calculus of structures does not rely on the notion of main connective and, like in term rewriting, it permits the application of the inference rules at any depth inside a formula. Tom is a pattern matching processor that integrates term rewriting facilities into imperative languages. In this paper, relying on the correspondence between the systems in the calculus of structures and term rewriting systems, we present an implementation of system BV of the calculus of structures in Java by exploiting the term rewriting features of Tom. This way, by means of the expressive power due to Java, it becomes possible to implement different search strategies. Since the systems in the calculus of structures follow a common scheme, we argue that our implementation can be generalized to other systems in the calculus of structures for classical logic, modal logics, and different fragments of linear logic. },
LANGUAGE = {Anglais },
AFFILIATION = {PROTHEO [INRIA Lorraine - LORIA] - Computer Science Institute,
University of Leipzig },
BOOKTITLE = {Structures and Deduction Structures and Deduction },
PAGES = {158-172 158-172 },
ADDRESS = {Lisbon },
TYPE = {Avec comit\'{e} de lecture },
EDITOR = {Bruscoli, Paola and Lamarche, François and Stewart, Charles},
NUMBER = {ISSN 1430-211X },
NOTE = {publi\'{e} Non },
DAY = {16},
MONTH = {07},
YEAR = {2005},
URL = {http://hal.inria.fr/inria-00000698/en/}
}
@INPROCEEDINGS{KIRCHNER:2005:43644,
TITLE = {Formal Validation of Pattern Matching Code },
AUTHOR = {Kirchner, Claude and Moreau, Pierre-Etienne and Reilles, Antoine},
ABSTRACT = {When addressing the formal validation of generated software, two main alternatives consist either to prove the correctness of compilers or to directly validate the generated code. Here, we focus on directly proving the correctness of compiled code issued from powerful pattern matching constructions typical of ML like languages or rewrite based languages such as ELAN, MAUDE or Tom. In this context, our first contribution is to define a general framework for anchoring algebraic pattern-matching capabilities in existing languages like C, Java or\ML. Then, using a just enough powerful intermediate language, we formalize the behavior of compiled code and define the correctness of compiled code with respect to pattern-matching behavior. This allows us to prove the equivalence of compiled code correctness with a generic first-order proposition whose proof could be achieved via a proof assistant or an automated theorem prover. We then extend these results to the multi-match situation characteristic of the ML like languages. The whole approach has been implemented on top of the Tom compiler and used to validate the syntactic matching code of the Tom compiler itself. },
KEYWORDS = {Compilation; pattern matching; multi-match; term rewriting; verified code },
LANGUAGE = {Anglais },
AFFILIATION = {PROTHEO [INRIA Lorraine - LORIA] },
BOOKTITLE = {Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming - PPDP'2005 Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming - PPDP'2005 },
PUBLISHER = {ACM },
PAGES = {187--197 187--197 },
ADDRESS = {Lisbon/Portugal },
TYPE = {Avec comit\'{e} de lecture },
EDITOR = {Barahone, Pedro and Felty, Amy },
NUMBER = {ISBN 1-59593-090-6 },
NOTE = {D.: Software publi\'{e} Non },
DAY = {11},
MONTH = {07},
YEAR = {2005},
URL = {http://hal.inria.fr/inria-00000701/en/}
}
This file has been generated by bibtex2html 1.75