Search

Your search keyword '"Cirstea, Horatiu"' showing total 50 results
Start Over Author "Cirstea, Horatiu" Language english

Refine your results

more »

more »

50 results on '"Cirstea, Horatiu"'

3. An Extension of PlusCal for Modeling Distributed Algorithms

Author

Alkayed, Heba, Cirstea, Horatiu, Merz, Stephan, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Merz, Stephan, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; The PlusCal language combines the expressive power of TLA+ with the “look and feel” of imperative pseudo-code in order to allow users to express algorithms at a high level of abstraction. PlusCal algorithms are translated to TLA+ specifications and can be formally verified using the TLA+ Toolbox. We propose a small extension of PlusCal, tentatively called Distributed PlusCal, intended for simplifying the presentation of distributed algorithms in PlusCal.Distributed systems consist of nodes that communicate by message passing. It is convenient to model a node as running several threads that share local memory. For example, one thread may execute the main algorithm, while a separate thread listens for incoming messages. Although PlusCal offers processes, they have a single thread of execution. Different threads of the same node must therefore be modeled as individual processes, and variables representing the local memory of a node must be declared as global variables, obscuring the structure of the code. Our first extension allows a PlusCal process to have several code blocks that execute in parallel. Besides, Distributed PlusCal explicitly identifies variables representing communication channels and introduces associated send and receive operations. In contrast to using ordinary variables and writing macros or operator definitions for channel operations, making channels part of the language gives us some more flexibility in the TLA+ translation.

Published
2020

12. Faithful (Meta-)Encodings Of Programmable Strategies Into Term Rewriting Systems

Author

Cirstea, Horatiu, Lenglet, Sergueï, Moreau, Pierre-Etienne, Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
FOS: Computer and information sciences, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computer Science - Programming Languages, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 0202 electrical engineering, electronic engineering, information engineering, F.4, 020207 software engineering, 020201 artificial intelligence & image processing, 02 engineering and technology, Programming Languages (cs.PL)
Abstract

Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and rewriting strategies are used to con- trol their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific strategies have been studied. We propose in this paper a generic encoding of classic control and traversal strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain term rewriting system. The encoding is proven sound and complete and, as a direct consequence, estab- lished termination methods used for term rewriting systems can be applied to analyze the termination of strategy controlled term rewriting systems. We show that the encoding of strategies into term rewriting systems can be easily adapted to handle many-sorted signa- tures and we use a meta-level representation of terms to reduce the size of the encodings. The corresponding implementation in Tom generates term rewriting systems compatible with the syntax of termination tools such as AProVE and TTT2, tools which turned out to be very effective in (dis)proving the termination of the generated term rewriting systems. The approach can also be seen as a generic strategy compiler which can be integrated into languages providing pattern matching primitives; experiments in Tom show that applying our encoding leads to performances comparable to the native Tom strategies., Logical Methods in Computer Science ; Volume 13, Issue 4 ; 1860-5974

Published
2017
Full Text
View/download PDF

13. Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation

Author

Cirstea, Horatiu and Escobar, Santiago

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer Science - Programming Languages, Programming Languages (cs.PL), Logic in Computer Science (cs.LO)
Abstract

This volume contains the formal proceedings of the Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), held on 23rd June 2016 in Porto, Portugal, as a satellite event of the First International Conference on Formal Structures for Computation and Deduction (FSCD 2016). The workshop brought together researchers working on program transformations, evaluation, and operationally based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area., Dedicated to the memory of Kristoffer H. Rose

Published
2017

15. A Java Framework for Test Data Generation

Author

Cirstea, Horatiu, Moreau, Pierre-Etienne, Balland, Emilie, Cirstea, Horatiu, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), Programming Language Technology For Communication Services (Phoenix), Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), and UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]

Subjects
[INFO]Computer Science [cs], [INFO] Computer Science [cs]
Published
2015

16. Towards an automatic tool for multi-scale model derivation

Author

Belkhir, Walid, Ratier, Nicolas, Nguyen, Duy Duc, Yang, Bin, Lenczner, Michel, Zamkotsian, Frédéric, Cirstea, Horatiu, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC), Laboratoire d'Astrophysique de Marseille (LAM), Aix Marseille Université (AMU)-Institut national des sciences de l'Univers (INSU - CNRS)-Centre National d'Études Spatiales [Toulouse] (CNES)-Centre National de la Recherche Scientifique (CNRS), Formal islands: foundations and applications (PAREO), Inria Nancy - Grand Est, Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), and Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS]
Abstract

This paper reports recent advances in the development of a symbolic asymptotic mod-eling software package, called MEMSALab, which will be used for automatic generation of asymptotic models for arrays of micro and nanosystems. More precisely, a model is a partial differential equation and an asymptotic method approximate it by another partial differential equation which can be numerically simulated in a reasonable time. The challenge consists in taking into account a wide range of different physical features and geometries e.g. thin structures, periodic structures, multiple nested scales etc. The main purpose of this software is to construct models incrementally so that model features can be included step by step. This idea, conceptualized under the name "by-extension-combination", is presented in detail for the first time.

Published
2015

17. A faithful encoding of programmable strategies into term rewriting systems

Author

Cirstea, Horatiu, Lenglet, Serguei, Moreau, Pierre-Etienne, Formal islands: foundations and applications (PAREO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Lenglet, Sergueï

Subjects
000 Computer science, knowledge, general works, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO.INFO-IR]Computer Science [cs]/Information Retrieval [cs.IR], Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing
Abstract

International audience; Rewriting is a formalism widely used in computer science and mathematical logic. When using rewriting as a programming or modeling paradigm, the rewrite rules describe the transformations one wants to operate and declarative rewriting strategies are used to control their application. The operational semantics of these strategies are generally accepted and approaches for analyzing the termination of specific strategies have been studied. We propose in this paper a generic encoding of classic control and traversal strategies used in rewrite based languages such as Maude, Stratego and Tom into a plain term rewriting system. The encoding is proven sound and complete and, as a direct consequence, established termination methods used for term rewriting systems can be applied to analyze the termination of strategy controlled term rewriting systems. The corresponding implementation in Tom generates term rewriting systems compatible with the syntax of termination tools such as AProVE and TTT2, tools which turned out to be very effective in (dis)proving the termination of the generated term rewriting systems. The approach can also be seen as a generic strategy compiler which can be integrated into languages providing pattern matching primitives; this has been experimented for Tom and performances comparable to the native Tom strategies have been observed. 1998 ACM Subject Classification F.4 Mathematical Logic and Formal Languages

Published
2015
Full Text
View/download PDF

18. Bringing Strategic Rewriting into the Mainstream

Author

Balland, Emilie, Cirstea, Horatiu, Moreau, Pierre-Etienne, Programming Language Technology For Communication Services (Phoenix), Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Formal islands: foundations and applications (PAREO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2], Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Moreau, Pierre-Etienne

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], pattern matching, strategies, term rewriting, object-oriented programming, tree traversal, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Abstract

Developing programming paradigms and languages that ease the program-mers' job of writing quality reusable code have been central ever since the beginning of programming. Tom, the language presented here, has been developed in an attempt to make a step forward in this direction. It promotes term rewriting techniques piggybacked on top of a general-purpose programming language like Java, C, and Python. This results in concise pieces of code which are close to the targeted application domain and which can be reasoned about using effective theoretical and practical tools. This approach has been validated on a variety of concrete applications ranging from academic tools like theorem provers, to large and complex applications, including the Tom compiler itself and several industrial products. This paper presents an overview of the current version of the language and explains the design rationale, browses the application domains and gives some hints on the tool building.

Published
2015

19. A constraint language for algebraic term based on rewriting theory

Author

Prugniel, François, Moreau, Pierre-Etienne, Cirstea, Horatiu, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Abstract

A key feature of Model Driven Engineering is the ability to define meta-models, but also constraints that have to be satisfied by their instances. Constraints are expressed in OCL (Object Constraint Language), which became a standard. OCL Constraints offer the possibility to capture properties which cannot be easily encoded in the meta-model. In the programming language community, instead of meta-models, we generally use grammars or algebraic signatures to define the syntax of the programs or abstract syntax trees (AST) we consider. But unfortunately, even when considering rich formalisms such as many-sorted signatures with subtyping or dependent types, they are not expressive enough to encode in a simple way some subsets of terms we want to consider. For instance arithmetic expressions which have at most two levels of plus operator, this includes a, a+b, (a+b)+(b+c), but not a+(b+(c+d)) for instance. There is a need for a constraint language dedicated to tree based data structures such as terms and AST. In this paper we present both a language to express constraints on trees, and a compilation scheme that shows how to translate constraints into an executable formalism based on term rewriting and strategies.

Published
2011

20. Rule-based Specification and Analysis of Security Policies

Author

Bourdier, Tony, Cirstea, Horatiu, Jaume, Mathieu, Kirchner, Hélène, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Sémantiques, preuves et implantation (SPI), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria), ANR-06-SETI-0016,SSURF,Sûreté et sécurité avec focal(2006), and Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)

Subjects
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], ComputingMilieux_MISCELLANEOUS, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

International audience

Published
2010

21. On Formal Specification and Analysis of Security Policies

Author

Bourdier, Tony, Cirstea, Horatiu, Jaume, Mathieu, Kirchner, Hélène, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Sémantiques, preuves et implantation (SPI), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria), ANR-06-SETI-0016,SSURF,Sûreté et sécurité avec focal(2006), and Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)

Subjects
security properties, access-control, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], security policy, constrained rewriting, first-order logical specification, reduction systems
Abstract

International audience; Security policies are ubiquitous in information systems and more generally in the management of sensitive information. Access control policies are probably the most largely used policies but their application goes well beyond this application domain. The enforcement of security policies is useless if some of their key properties like the consistency, for example, cannot be stated and checked. We propose here a framework where the security policies and the systems they are applied on, are specified separately but using a common formalism. This separation allows us not only some analysis of the policy independently of the target system but also the application of a given policy on different systems. Besides the abstract formalism we also explore how rewrite and reduction systems can be used and combined in a rather systematic way to provide executable specifications for this framework. We also propose a notion of system and policy transformation that gives the possibility to study some properties which cannot be expressed only within the initial presentation. We have shown, in particular, how confidentiality, integrity and confinment can be expressed for the BLP policy that does not deal explicitly with information flows but only with objects containing tractable information.

Published
2010

22. Constrained rewriting in recognizable theories

Author

Bourdier, Tony, Cirstea, Horatiu, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), ANR-06-SETI-0016,SSURF,Sûreté et sécurité avec focal(2006), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Computer Science::Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science::Symbolic Computation, Pattern matching, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Rewrite systems, Tree automata
Abstract

Rewriting has long been shown useful for equational reasoning but its expressive power is not always appropriate for certain situations, as for instance for specifying partial functions and exceptions or when dealing with relations over terms. That is why some generalizations of rewriting, such as ordered rewriting, class rewriting, strategic rewriting, conditional or constrained rewriting, have emerged. In particular, constraints over terms are very suitable to define sets of terms thanks to logic formulae. Most of the works on constrained rewriting focus on order, equality, disequality and membership constraints. We extend in this paper the usual notion of constrained rewrite systems by constraining rules not only with classical constraints but with any first order formula and perform rewriting according to an interpretation of functional and predicate symbols. We then show that the specification of such interpretations with tree automata offers us a framework sufficiently powerful to build an algorithm for solving a particular case of constrained matching.

Published
2010

23. Analysis of Lattice-Based Access Control Policies using Rewiting Systems and Tom

Author

Bourdier, Tony, Cirstea, Horatiu, Moreau, Pierre-Etienne, Santana De Oliveira, Anderson, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), S. Mauw and L. van der Torre (eds), ANR-06-SETI-0016,SSURF,Sûreté et sécurité avec focal(2006), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

International audience; In this paper we show how access control policies can be specified using term rewriting systems and present the corresponding implementation realized using the Tom framework. We focus on two well known models (Bell-Lapadula and McLean) and propose an algorithm that detects potential information leakages, i.e. checks that information can be accessed only by authorized users independently of the actions performed in a given system.

Published
2009

24. Distributive rewriting calculus

Author

Cirstea, Horatiu, Houtmann, Clement, Wack, Benjamin, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and Grit Denker and Carolyn L. Talcott

Subjects
ACM: D.: Software/D.1: PROGRAMMING TECHNIQUES, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, ACM: D.: Software/D.3: PROGRAMMING LANGUAGES, Computer Science::Programming Languages
Abstract

International audience; 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.

Published
2006

25. Production Systems and Rete Algorithm Formalisation

Author

Cirstea, Horatiu, Kirchner, Claude, Moossen, Michael, Moreau, Pierre-Etienne, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
production rules, matching, term rewriting, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], business rule, réécriture de terme, réseau rete, règles de production, filtrage, rete network, règles métiers, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

Rapport de contrat.; 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.

Published
2004

26. Rule based programming in Java for protocol verification

Author

Cirstea, Horatiu, Moreau, Pierre-Etienne, Reilles, Antoine, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Narciso Marti-Oliet, and Narciso Marti-Oliet and Manuel Clavel and Alberto Verdejo

Subjects
[INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], model-checking, modèle de vérification, rewriting, réécriture
Abstract

Colloque avec actes et comité de lecture. internationale.; International audience; 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.

Published
2004

27. Production Systems and Rewrite Systems

Author

Cirstea, Horatiu, Kirchner, Claude, Moossen, Michael, Moreau, Pierre-Etienne, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
production rules, associative-commutative matching, filtrage associatif-commutatif, matching constraint, term rewriting, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], business rule, réécriture de terme, règles de production, règles métiers, contrainte de filtrage
Abstract

Rapport de contrat.; 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.

Published
2004

28. Types for Web Rule Languages: a preliminary study

Author

Cirstea, Horatiu, Coquery, Emmanuel, Drabent, Wlodzimierz, Fages, Francois, Kirchner, Claude, Maluszynski, Jan, Wack, Benjamin, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Constraint programming (CONTRAINTES), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Polska Akademia Nauk = Polish Academy of Sciences (PAN), Department of Computer and Information Science - Linköping University, Linköping University (LIU), Inria, and Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)

Subjects
contraintes, type system, constraint, rule based language, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], système de type, langage à base de règle, rewriting, réécriture
Abstract

Rapport de contrat.; We survey and analyse the relevant existing work on typing of rules, in particular on typing of constraint logic programs and discuss applicability of these approaches to the rewerse reasoning and query languages under development by WG I1 and by WG I4. This is related to WG I1, developing logic programming like languages for reasoning on the web and with WG I4 investigating development of declarative query languages such as XPathLog and Xcerpt.

Published
2004

29. The rho cube : some results, some problems

Author

Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi, Wack, Benjamin, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems (LOGNET), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Objects, types and prototypes : semantics and validation (MIRHO), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), D. Kesner, T. Nipkow and F. van Raamsdonk, and Loria, Publications

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], lambda calculus, unicité du type, théorie des types, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], rewriting, cube de barendregt, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], Computer Science::Logic in Computer Science, type theory, uniqueness of typing, rewriting calculus, calcul de réécriture, lambda calcul, barendregt's cube, réécriture
Abstract

Held in conjunction with FLOC'02. Colloque avec actes informels avec comité de lecture. internationale.; International audience; The rewriting 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 calculu breaks the confluence property, so that we need to define appropiate 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. Uniqueness of typing is generally no longer valid but we can still prove it for one of the most restrictive systems, rho-> and rho2.

Published
2002

32. The Rewriting Calculus - Part I

Author

Cirstea, Horatiu, Kirchner, Claude, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Logic, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, non-determinism, filtrage, calcul de réécriture, rule based language, rewriting-calculus, lambda calcul, stratégie, matching, non-déterminisme, lambda-calculus, rewriting, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, langage à base de règles, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, strategy, réécriture
Abstract

Article dans revue scientifique avec comité de lecture.; 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 confluence of the calculus.

Published
2001
Full Text
View/download PDF

33. Rewriting and Multisets in Rho-calculus and ELAN

Author

Cirstea, Horatiu, Kirchner, Claude, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
multisets, stratégie, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, matching, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], multi-ensembles, Computer Science::Programming Languages, filtrage, strategy, réécriture, rewriting
Abstract

ISSN: 1453-8245. Article dans revue scientifique avec comité de lecture.; The 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 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 . We show how the set-like data structures are easily represented in ELAN and how this can be used in order to specify the Needham-Schroeder public-key protocol.

Published
2001

34. Rewriting and Multisets in the Rewriting Calculus and ELAN

Author

Cirstea, Horatiu, Kirchner, Claude, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
stratégie, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, matching, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Computer Science::Programming Languages, multiset, filtrage, strategy, réécriture, rewriting
Abstract

Colloque avec actes sans comité de lecture. internationale.; International audience; 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.

Published
2000

35. The Rewriting Calculus

Author

Cirstea, Horatiu, Kirchner, Claude, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, rule based language, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, matching, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Computer Science::Programming Languages, non-determinism, lambda-calculus, strategy, rewriting-calculus, rewriting
Abstract

Rapport interne.; 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 paper 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.

Published
2000

36. A Rho Cube

Author

Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems (LOGNET), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Environment for cooperation (ECOO), Objects, types and prototypes : semantics and validation (MIRHO), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, systèmes de type, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, type systems, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], réécriture, rewriting
Abstract

Aussi apparu en "Proc. of FOSSACS, Foundations of Software Science and Computation Structures Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2-6, Lecture Notes in Computer Sciences, no 2. Rapport interne.; 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 (LF) of Harper-Honsell-Plotkin, and of the Calculus of Constructions (CC) of Coquand-Huet.

Published
2000

37. Specifying Authentication Protocols Using ELAN

Author

Cirstea, Horatiu, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, rewrite rules, authentication protocol, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], protocoles d'authentification, stratégies, règles de réécriture
Abstract

Colloque avec actes sans comité de lecture.; Programming with rewrite rules and strategies has been already used for describing several computational logics. In this paper is described the way the Needham-Schroeder Public-Key protocol is specified in ELAN, the system developed in Nancy for executing rewrite programs. The protocol aims to establish a mutual authentication between an initiator and a responder that communicate via an insecure network. The protocol has been shown vulnerable and a correction has been proposed by G. Lowe. The behavior of the agents and of the intruders as well as the security invariants the protocol should verify are naturally described by conditional rewrite rules. The application of the rewrite rules is controlled by strategies. Similar attacks to those already described in the literature have been discovered. We show how different strategies using the same set of rewrite rules can improve the efficiency in finding the attacks and we compare our results to existing approaches.

Published
1999

38. Combining Higher-Order and First-Order Computation Using Rho Calculus: Towards a Semantics of ELAN

Author

Cirstea, Horatiu, Kirchner, Claude, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, non-déterminisme, substitutions explicites, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Computer Science::Programming Languages, Computer Science::Symbolic Computation, non-determinism, réécriture, explicit substitutions, rewriting
Abstract

Colloque sur invitation.; The recently introduced rewriting calculus permits to express in a uniform and simple way first-order rewriting, lambda-calculus and non-deterministic computations as well as their combination. In this work, we recall the main properties of the rewriting calculus and we give a full first-order presentation of this rewriting calculus using an explicit substitution setting that generalizes the lambda-sigma-calculus. Its basic properties in the untyped as well as typed cases are presented. We then detail how to use the rewriting calculus to give an operational semantics to the rewrite based language ELAN.

Published
1998

39. Combining Higher-Order & First-Order Computation Using $\rho$-calculus: Towards a semantics of ELAN Full-version

Author

Cirstea, Horatiu, Kirchner, Claude, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
substitutions explicites, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], $\lambda$-calculus, $\lambda$-calcul, Data_CODINGANDINFORMATIONTHEORY, explicit substitutions, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, non-deterministic computations, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, réécriture du premier ordre, Computer Science::Programming Languages, first-order rewriting, computations non-déterministe
Abstract

Rapport interne.; The recently introduced $\rho$-calculus permits to express in a uniform and simple way first-order rewriting, $\lambda$-calculus and non-deterministic computations as well as their combination. In this work, we emphasize the expressiveness of $\rho$-calculus and we give a full first-order presentation of this rewriting calculus using an explicit substitution setting $\rho\sigma$ that generalizes the $\lambda\sigma$-calculus. Its basic properties in the untyped as well as typed cases are presented. We then detail how to use the $\rho$-calculus to give an operational semantics to the rewrite based language Elan.

Published
1998

40. Using Rewriting and Strategies for Describing the B Predicate Prover

Author

Cirstea, Horatiu, Kirchner, Claude, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and F. Pfenning, B. Gramlich

Subjects
stratégie, règle de réécriture, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], prouveur de propositionsrègles de réécriture, stratégies, predicate calculus, règles de réécriture, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, prouveur de propositions, calcul de predicat, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, propositional prover, rewriting rules, rewrite rule, strategy
Abstract

Colloque avec actes sans comité de lecture.; The framework of computational systems has been already used for describing several computational logics. In this paper is described the way a propositional prover and a predicate prover are implemented in ELAN, the system developed in Nancy for describing and executing computational systems. The inference rules for the provers are described by conditional rewrite rules and their application is controlled by strategies. We show how different strategies using the same set of rewrite rules can yield different proof methods.

Published
1998

41. $\rho$-Calculus. Its Syntax and Basic Properties

Author

Cirstea, Horatiu, Kirchner, Claude, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Rewriting, Explicit substitution, $\rho$-calculus, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], $\lambda$-calculus, Réécriture, $\lambda$-calcul, Substitution explicite, ELAN, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Filtrage, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, $\rho$-calcul, Computer Science::Programming Languages, Matching, Stratégies
Abstract

Rapport interne.; \roCal\ is a new calculus that integrates in a uniform and simple setting first-order rewriting, $\lambda$-calculus and non-deterministic computations. This paper describes the calculus from its syntax to its basic properties in the untyped case. We show how it embeds first-order rewriting & $\lambda$-calculus. Finally we use \roCal\ to give an operational semantics to the rewrite based language \elan.

Published
1998

44. TomML: A Rule Language for Structured Data.

Author

Cirstea, Horatiu, Moreau, Pierre-Etienne, and Reilles, Antoine

Abstract

We present the Tom language that extends Java with the purpose of providing high level constructs inspired by the rewriting community. Tom bridges thus the gap between a general purpose language and high level specifications based on rewriting. This approach was motivated by the promotion of rule based techniques and their integration in large scale applications. Powerful matching capabilities along with a rich strategy language are among Tom΄s strong features that make it easy to use and competitive with respect to other rule based languages. Tom is thus a natural choice for querying and transforming structured data and in particular XML documents [1]. We present here its main XML oriented features and illustrate its use on several examples. [ABSTRACT FROM AUTHOR]

Published
2009
Full Text
View/download PDF

45. Confluence of Pattern-Based Calculi.

Author

Hutchison, David, Kanade, Takeo, Kittler, Josef, Kleinberg, Jon M., Mattern, Friedemann, Mitchell, John C., Naor, Moni, Nierstrasz, Oscar, Pandu Rangan, C., Steffen, Bernhard, Sudan, Madhu, Terzopoulos, Demetri, Tygar, Doug, Vardi, Moshe Y., Weikum, Gerhard, Baader, Franz, Cirstea, Horatiu, and Faure, Germain

Abstract

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. We propose here 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. [ABSTRACT FROM AUTHOR]

Published
2007
Full Text
View/download PDF

47. The Rho Cube.

Author

Goos, Gerhard, Hartmanis, Juris, van Leeuwen, Jan, Honsell, Furio, Miculan, Marino, Cirstea, Horatiu, Kirchner, Claude, and Liquori, Luigi

Abstract

The rewriting calculus, or Rho Calculus (ρCal), is a simple calculus that uniformly integrates abstraction on patterns and non- determinism. Therefore, it fully integrates rewriting and λ-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 à la Church, together with nine (8+1) type systems which can be placed in a ρ-cube that extends the λ-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 "λ" and "∏" abstractors. As a consequence, this brings matching and rewriting as the first class concepts of the Rho-versions of the Logical Framework (LF) of Harper-Honsell-Plotkin, and of the Calculus of Constructions (CC) of Coquand-Huet. [ABSTRACT FROM AUTHOR]

Published
2001
Full Text
View/download PDF

48. Anti-patterns for rule-based languages

Author

Cirstea, Horatiu, Kirchner, Claude, Kopetz, Radu, and Moreau, Pierre-Etienne

Subjects
*RULE-based programming, *PROGRAMMING languages, *CONSTRAINT programming, *SOFTWARE patterns, *COMPUTER software development, *PATTERN recognition systems
Abstract

Abstract: Negation is intrinsic to human thinking and most of the time when searching for something, we base our patterns on both positive and negative conditions. This should be naturally reflected in software that provide pattern-based searches. We would like for example to specify that we search for white cars that are not station wagons, or that we search for a list of objects that does not contain two identical elements. In this paper we extend the notion of pattern to the one of anti-pattern, i.e. patterns that may contain complement symbols. This concept is appropriate to design powerful extensions to pattern-based programming languages like Ml, Asf+Sdf, Stratego, Maude, Elan or Tom and we show how this is used to extend the expressiveness and usability of the Tom language. We further define formally the semantics of anti-patterns both in the syntactic case, i.e. when the symbols have no specific theory associated, and modulo an arbitrary equational theory . We then extend the classical notion of matching between patterns and ground terms to matching between anti-patterns and ground terms. Solving such problems can be performed either using general techniques as disunification, which we exemplify in the syntactical case, or more tailored and efficient approaches, which we chose to illustrate on the specific and very useful case of associativity, possibly with a unity. This allows us to be generic enough to give in this framework a very simple and natural expression of, for instance, the AllDiff standard predicate of constraint programming. [Copyright &y& Elsevier]

Published
2010
Full Text
View/download PDF

50. TomML: A Rule Language For Structured Data

Author

Horatiu Cirstea, Pierre-Etienne Moreau, Antoine Reilles, Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and Cirstea, Horatiu

Subjects
Matching (statistics), [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Java, Programming language, Computer science, computer.internet_protocol, 020207 software engineering, Rule-based system, 02 engineering and technology, General-purpose language, computer.software_genre, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], Data model, 0202 electrical engineering, electronic engineering, information engineering, Natural (music), 020201 artificial intelligence & image processing, Rewriting, Pattern matching, computer, XML, computer.programming_language
Abstract

International audience; We present the Tom language that extends Java with the purpose of providing high level constructs inspired by the rewriting community. Tom bridges thus the gap between a general purpose language and high level specifications based on rewriting. This approach was motivated by the promotion of rule based techniques and their integration in large scale applications. Powerful matching capabilities along with a rich strategy language are among Tom's strong features that make it easy to use and competitive with respect to other rule based languages. Tom is thus a natural choice for querying and transforming structured data and in particular XML documents. We present here its main XML oriented features and illustrate its use on several examples.

Published
2009

Catalog

Books, media, physical & digital resources
See catalog results