@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -oc tmp/citeAntoine.Reilles -ob tmp/Antoine.Reilles.bib -c 'author:"Reilles, Antoine"' biblio/complete.bib}}
@TECHREPORT{reilles03a,
CRINNUMBER = {A03-R-383},
EQUIPE = {PROTHEO},
AUTHOR = {Reilles, Antoine},
TITLE = {Réécriture dans un cadre concurrent},
INSTITUTION = {INPL},
YEAR = {2003},
TYPE = {Stage de DEA},
MONTH = {Jul},
URL = {http://www.loria.fr/publications/2003/A03-R-383/A03-R-383.ps},
KEYWORDS = {rewriting, concurrency, strategies},
ABSTRACT = {Ce document décrit une proposition de système de stratégies permettant la mise en oeuvre de parallélisme pour des systèmes de réécriture avec le système TOM.}
}
@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. }
}
@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.}
}
@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