Bibliography

• 1E. Balland, C. Kirchner, P.-E. Moreau.
  
  Formal Islands, in: 11th International Conference on Algebraic Methodology and Software Technology, Kuressaare, Estonia, M. Johnson, V. Vene (editors), LNCS, Springer-Verlag, jul 2006, vol. 4019, p. 51–65.
  
  http://www.loria.fr/~moreau/Papers/BallandKM-AMAST2006.pdf
• 2G. Barthe, H. Cirstea, C. Kirchner, L. Liquori.
  
  Pure Patterns Type Systems, in: Principles of Programming Languages - POPL2003, New Orleans, USA, ACM, Jan 2003, p. 250–261.
• 3G. Bonfante, Y. Guiraud.
  
  Polygraphic programs and polynomial-time functions, in: Logical Methods in Computer Science, 2009, vol. 5, n^o 2:14, p. 1-37.
• 4P. Brauner, C. Houtmann, C. Kirchner.
  
  Principles of Superdeduction, in: Twenty-Second Annual IEEE Symposium on Logic in Computer Science - LiCS 2007, Wroclaw Pologne, IEEE Computer Society, 2007.
  
  http://dx.doi.org/10.1109/LICS.2007.37
• 5H. Cirstea, C. Kirchner.
  
  The rewriting calculus - Part I and II, in: Logic Journal of the Interest Group in Pure and Applied Logics, May 2001, vol. 9, n^o 3, p. 427-498.
• 6Y. Guiraud.
  
  Termination orders for 3-dimensional rewriting, in: Journal of Pure and Applied Algebra, 2006, vol. 207, n^o 2, p. 341-371.
• 7Y. Guiraud, P. Malbos.
  
  Higher-dimensional categories with finite derivation type, in: Theory and Applications of Categories, 2009, vol. 22, n^o 18, p. 420-478.
• 8C. Kirchner, R. Kopetz, P.-E. Moreau.
  
  Anti-Pattern Matching, in: 16th European Symposium on Programming, Braga, Portugal, Lecture Notes in Computer Science, Springer, 2007, vol. 4421, p. 110–124.
  
  http://www.loria.fr/~moreau/Papers/KirchnerKM-2007.pdf
• 9P.-E. Moreau, C. Ringeissen, M. Vittek.
  
  A Pattern Matching Compiler for Multiple Target Languages, in: 12th Conference on Compiler Construction, Warsaw (Poland), G. Hedin (editor), LNCS, Springer-Verlag, may 2003, vol. 2622, p. 61–76.
  
  http://www.loria.fr/~moreau/Papers/MoreauRV-CC2003.ps.gz

Doctoral Dissertations and Habilitation Theses

• 10T. Bourdier.
  
  Méthodes algébriques pour la formalisation et l'analyse de politiques de sécurité, Université Henri Poincaré, october 2011, tel-00646401.
• 11C. Roux.
  
  Terminaison à base de tailles: Sémantique et généralisations, Université Henri Poincaré - Nancy I, June 2011.
  
  http://hal.inria.fr/tel-00606360/en

Articles in International Peer-Reviewed Journal

• 12T. Bourdier.
  
  Specification, analysis and transformation of security policies via rewriting techniques, in: Journal of Information Assurance and Security, 2011, vol. 6, n^o 5, p. 357-368.
  
  http://hal.inria.fr/inria-00525761/en
• 13Y. Guiraud, P. Malbos.
  
  Coherence in monoidal track categories, in: Mathematical Structures in Computer Science, 2011, 32 pages, to appear.
• 14Y. Guiraud, P. Malbos.
  
  Higher-dimensional normalisation strategies for acyclicity, in: Advances in Mathematics, 2011, 46 pages, accepted.
• 15Y. Guiraud, P. Malbos.
  
  Identities among relations for higher-dimensional rewriting systems, in: Société Mathématique de France, Séminaires et Congrès, 2011, vol. 26, p. 145-161.
  
  http://hal.inria.fr/hal-00426228/en

International Conferences with Proceedings

• 16T. Bourdier.
  
  Tree automata based semantics of firewalls, in: 6th International Conference on Network Architectures and Information Systems Security, La Rochelle, France, IEEE, 2011, p. pp.171–178. [ DOI : 10.1109/SAR-SSI.2011.5931363 ]
  
  http://hal.inria.fr/inria-00460462/en
• 17T. Bourdier, H. Cirstea.
  
  Symbolic analysis of network security policies using rewrite systems, in: Symposium on Principles and Practices of Declarative Programming, Odense, Denmark, ACM, 2011, p. pp.77-88. [ DOI : 10.1145/2003476.2003489 ]
  
  http://hal.inria.fr/inria-00567858/en
• 18T. Bourdier, H. Cirstea, M. Jaume, H. Kirchner.
  
  Formal Specification and Validation of Security Policies, in: Foundations & Practice of Security, Paris, France, J. Garcia-Alfaro, P. Lafourcade (editors), Lecture Notes in Computer Science, Springer, Heidelberg, 2011, vol. 6888, p. 148-163.
  
  http://hal.inria.fr/inria-00507300/en
• 19C. Houtmann.
  
  Superdeduction in Lambda-bar-mu-mu-tilde, in: Classical Logic and Computation 2010, Brno, Czech Republic, S. van Bakel, S. Berardi, U. Berger (editors), 2011, vol. 47, p. 33-43. [ DOI : 10.4204/EPTCS.47.5 ]
  
  http://hal.inria.fr/inria-00498744/en
• 20C. Roux.
  
  Refinement types as higher order dependency pairs, in: 222nd International Conference on Rewriting Techniques and Applications : RTA'11, Novi Sad, Serbia, LIPics, May 2011, vol. 10, p. 299-312.
  
  http://hal.inria.fr/inria-00598567/en
• 21S. Stratulat, V. Demange.
  
  Automated Certification of Implicit Induction Proofs, in: Certified Programs and Proofs, Kenting, Taïwan, Province De Chine, 2011.
  
  http://hal.inria.fr/hal-00644876/en/

Internal Reports

• 22J.-C. Bach, P.-E. Moreau, M. Pantel, X. Crégut.
  
  Model Transformations with Tom, November 2011.
  
  http://hal.inria.fr/hal-00646350/en
• 23F. Prugniel, P.-E. Moreau, H. Cirstea.
  
  A constraint language for algebraic term based on rewriting theory, November 2011.
  
  http://hal.inria.fr/hal-00646343/en
• 24C. Roux.
  
  Refinement Types as Higher Order Dependency Pairs, January 2011.
  
  http://hal.inria.fr/inria-00552046/en
• 25C. Tavares.
  
  A type system for embedded rewriting languages with associative pattern matching: from theory to practice, November 2011.
  
  http://hal.inria.fr/hal-00643808/en

Other Publications

• 26S. Gaussent, Y. Guiraud, P. Malbos.
  
  Polygraphs and actions of monoids on categories, 2011, preprint, 56 pages.

• 27J.-C. Bach, E. Balland, P. Brauner, R. Kopetz, P.-E. Moreau, A. Reilles.
  
  Tom Manual, LORIA, 2009.
  
  http://hal.inria.fr/inria-00121885/en/
• 28E. Balland, P. Brauner, R. Kopetz, P.-E. Moreau, A. Reilles.
  
  Tom: Piggybacking rewriting on java, in: 18th International Conference on Rewriting Techniques and Applications - (RTA), Paris, France, Lecture Notes in Computer Science, jun 2007, vol. 4533, p. 36-47.
• 29G. Bonfante, Y. Guiraud.
  
  Intensional properties of polygraphs, in: Electronic Notes in Theoretical Computer Science, 2008, vol. 203, n^o 1, p. 65-77.
• 30P. Borovanský, C. Kirchner, H. Kirchner.
  
  Controlling Rewriting by Rewriting, in: Proceedings of the first international workshop on rewriting logic - (WRLA), Asilomar (California), J. Meseguer (editor), Electronic Notes in Theoretical Computer Science, sep 1996, vol. 4.
• 31P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau.
  
  ELAN from a rewriting logic point of view, in: Theoretical Computer Science, Jul 2002, vol. 2, n^o 285, p. 155-185.
• 32A. Burroni.
  
  Higher-dimensional word problems with applications to equational logic, in: Theoretical Computer Science, 1993, vol. 115, n^o 1, p. 43-62.
• 33H. Cirstea.
  
  Le calcul de réécriture, Université Nancy II, October 2010, Habilitation à Diriger des Recherches.
  
  http://hal.inria.fr/tel-00546917/en
• 34E. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain.
  
  Certification of Automated Termination Proofs, in: Frontiers of Combining Systems, 2007, p. 148–162.
• 35J.-Y. Girard, Y. Lafont, P. Taylor.
  
  Proofs and Types, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989, vol. 7.
• 36Y. Guiraud.
  
  Présentations d'opérades et systèmes de réécriture, Université Montpellier 2, 2004.
• 37Y. Guiraud.
  
  The three dimensions of proofs, in: Annals of Pure and Applied Logic, 2006, vol. 141, n^o 1-2, p. 266-295.
• 38Y. Guiraud.
  
  Two polygraphic presentations of Petri nets, in: Theoretical Computer Science, 2006, vol. 360, n^o 1-3, p. 124-146.
• 39Y. Guiraud.
  
  Polygraphs for termination of left-linear term rewriting systems, 2007, Preprint.
• 40C. B. Jay, D. Kesner.
  
  First-class patterns, in: Journal of Functional Programming, 2009, vol. 19, n^o 2, p. 191-225.
• 41J.-P. Jouannaud, H. Kirchner.
  
  Completion of a set of rules modulo a set of Equations, in: SIAM J. of Computing, 1986, vol. 15, n^o 4, p. 1155–1194.
• 42J.-P. Jouannaud, C. Kirchner.
  
  Solving equations in abstract algebras: a rule-based survey of unification, in: Computational Logic. Essays in honor of Alan Robinson, Cambridge (MA, USA), J.-L. Lassez, G. Plotkin (editors), The MIT press, Cambridge (MA, USA), 1991, chap. 8, p. 257–321.
• 43G. Kahn.
  
  Natural Semantics, INRIA Sophia-Antipolis, feb 1987, n^o 601.
• 44C. Kirchner, H. Kirchner, M. Vittek.
  
  Designing Constraint Logic Programming Languages using Computational Systems, in: Proc. 2nd CCL Workshop, La Escala (Spain), F. Orejas (editor), sep 1993.
• 45H. Kirchner, P.-E. Moreau.
  
  Promoting Rewriting to a Programming Language: A Compiler for Non-Deterministic Rewrite Programs in Associative-Commutative Theories, in: Journal of Functional Programming, 2001, vol. 11, n^o 2, p. 207-251.
  
  http://www.loria.fr/~moreau/Papers/jfp.ps.gz
• 46J. W. Klop, V. van Oostrom, R. de Vrijer.
  
  Lambda calculus with patterns, in: Theor. Comput. Sci., 2008, vol. 398, n^o 1-3, p. 16–31.
• 47P.-E. Moreau.
  
  Programmation et confiance, Institut National Polytechnique de Lorraine - INPL, 06 2008.
  
  http://tel.archives-ouvertes.fr/tel-00337408/en/
• 48P.-E. Moreau, A. Reilles.
  
  Rules and Strategies in Java, in: 7th International Workshop on Reduction Strategies in Rewriting and Programming - WRS 2007 Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007) Electronic Notes in Theoretical Computer Science, France Paris, J. Giesl (editor), Elsevier, 2008, vol. 204, p. 71-82.
  
  http://hal.inria.fr/inria-00185698/en/
• 49P.-E. Moreau, C. Ringeissen, M. Vittek.
  
  A Pattern Matching Compiler for Multiple Target Languages, in: 12th Conference on Compiler Construction - (CC), G. Hedin (editor), Lecture Notes in Computer Science, Springer-Verlag, MAY 2003, vol. 2622, p. 61–76.
• 50S. Peyton-Jones.
  
  The implementation of functional programming languages, Prentice-Hall, 1987.
• 51C. Rabadan, F. Klay.
  
  Un nouvel algorithme de contrôle de conformité pour la capacité de transfert `Available Bit Rate', CNET, 1997, n^o NT/CNET/5476.
• 52M. Rusinowitch, S. Stratulat, F. Klay.
  
  Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm, in: CAV, E. A. Emerson, A. P. Sistla (editors), Lecture Notes in Computer Science, Springer, 2000, vol. 1855, p. 344-357.
• 53M. Rusinowitch, S. Stratulat, F. Klay.
  
  Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm, in: J. Autom. Reasoning, 2003, vol. 30, n^o 2, p. 53-177.
• 54N. Shankar, S. Owre, J. M. Rushby, D. W. J. Stringer-Calvert.
  
  PVS prover guide - version 2.4, SRI International, November 2001.
• 55S. Stratulat.
  
  Integrating Implicit Induction Proofs into Certified Proof Environments, in: Integrated Formal Methods - IFM 2010, Nancy, France, D. Mery, S. Merz (editors), Lecture Notes in Computer Science, Springer Berlin / Heidelberg, October 2010, vol. 6396, p. 320-335, The original publication is available at www.springerlink.com..
  
  http://hal.inria.fr/inria-00525187/en/
• 56M. van den Brand, A. van Deursen, P. Klint, S. Klusener, E. A. van der Meulen.
  
  Industrial Applications of ASF+SDF, in: AMAST '96, M. Wirsing, M. Nivat (editors), Lecture Notes in Computer Science, Springer-Verlag, 1996, vol. 1101, p. 9-18.