, A meta-environment for generating programming environments, ACM Transactions on Software Engineering and Methodology, vol.2, pp.176-201, 1993.
, Maude: Specification and programming in rewriting logic, Theoretical Computer Science, vol.285, pp.187-243, 2002.
, An overview of the Cafe specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks, Proceedings of the 1st IEEE International Conference on Formal Engineering Methods, p.170, 1997.
, of Electronic Notes in Theoretical Computer Science, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, vol.15, pp.55-70, 1998.
, A Pattern Matching Compiler for Multiple Target Languages, Proceedings of the 12th Conference on Compiler Construction, vol.2622, pp.61-76, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099427
, CARIBOO : An induction based proof tool for termination with strategies, Proceedings of the 4th International Conference on Principles and Practice of Declarative Programming, pp.62-73, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00107557
, of Electronic Notes in Theoretical Computer Science, Selected papers of the 4th International Workshop on Strategies in Automated Deduction, vol.58, pp.155-188, 2001.
, of Electronic Notes in Theoretical Computer Science, Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications, vol.71, pp.188-207, 2002.
, Termination of rewriting strategies: a generic approach, Proceedings of the APPSEM II Workshop, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000178
, Termination of rewriting under strategies, ACM Transactions on Computational Logic, vol.10, issue.2, pp.1-52, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00182432
, A proof of weak termination providing the right way to terminate, Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing, vol.3407, pp.356-371, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00100120
, Computing Constructor Forms with Non Terminating Rewrite Programs, Proceedings of the 8th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming, pp.121-132, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00112083
, Narrowing, abstraction and constraints for proving properties of reduction relations, Rewriting, Computation and Proof. Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, vol.4600, pp.44-67, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00182434
, Relating innermost, weak, uniform and modular termination of term rewriting systems, Proceedings of the 3rd International Conference on Logic Programming and Automated Reasoning, vol.624, pp.285-296, 1992.
DOI : 10.1007/bfb0013069
URL : https://kluedo.ub.uni-kl.de/files/349/seki_26.pdf
, On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems, Theoretical Computer Science, vol.165, issue.1, pp.97-131, 1996.
DOI : 10.1016/0304-3975(96)00042-4
URL : https://doi.org/10.1016/0304-3975(96)00042-4
, A proof of weak termination of typed lambda-sigmacalculi, Proceedings of the Workshop Types for Proofs and Programs, vol.1512, pp.134-153, 1998.
DOI : 10.1007/bfb0097790
, Proceedings of the 15th International Workshop in Computer Science Logic, vol.2142, pp.484-498, 2001.
, Computations in orthogonal rewriting systems, I, Computational Logic, pp.395-414, 1991.
, Inductionless induction, Handbook of Automated Reasoning, vol.I, pp.913-962, 2001.
DOI : 10.1016/b978-044450813-3/50016-3
URL : http://www.lsv.ens-cachan.fr/~comon/ftp.articles/hb.ps
, Proofs by induction in equational theories with constructors, preliminary version in Proceedings of the 21st Symposium on Foundations of Computer Science, vol.25, pp.239-266, 1980.
DOI : 10.1016/0022-0000(82)90006-x
URL : https://hal.archives-ouvertes.fr/inria-00076533
, A decidability result about sufficient completeness of axiomatically specified abstract data types, Proceedings of the 6th GI-Conference on Theoretical Computer Science, vol.145, pp.257-267, 1982.
DOI : 10.1007/bfb0036486
, Completeness in data type specifications, Proceedings of the EUROCAL Conference, vol.204, pp.348-362, 1985.
, Proof by induction using test sets, Proceedings of the 8th International Conference on Automated Deduction, vol.230, pp.99-117, 1986.
DOI : 10.1007/3-540-16780-3_83
, Proceedings of the 8th International Conference on Automated Deduction, vol.230, pp.128-140, 1986.
, Automatic proofs by induction in theories without constructors, Information and Computation, vol.82, pp.1-33, 1989.
DOI : 10.1016/0890-5401(89)90062-x
URL : https://doi.org/10.1016/0890-5401(89)90062-x
, Tools for proving inductive equalities, relative completeness and ?-completeness, Information and Computation, vol.84, issue.1, pp.47-70, 1990.
DOI : 10.1016/0890-5401(90)90033-e
URL : https://doi.org/10.1016/0890-5401(90)90033-e
, Using induction and rewriting to verify and complete parameterized specifications, Theoretical Computer Science, vol.170, issue.1-2, pp.245-276, 1996.
DOI : 10.1016/s0304-3975(96)80708-0
URL : https://doi.org/10.1016/s0304-3975(96)80708-0
, Automatic verification of. sufficient completeness for. specifications of complex data structures, INRIA, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00578926
, Automatic Verification of Sufficient Completeness for Conditional Constrained Term Rewriting Systems, INRIA, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00070163
, The Maude sufficient completeness checker
, Semantic confluence tests and completion methods, Information and Control, vol.65, pp.182-215, 1985.
DOI : 10.1016/s0019-9958(85)80005-x
URL : https://doi.org/10.1016/s0019-9958(85)80005-x
, On sufficient completeness and related properties of term rewriting systems, Acta Informatica, vol.24, pp.395-415, 1987.
DOI : 10.1007/bf00292110
, Testing for the ground (co-)reducibility property in termrewriting systems, Theoretical Computer Science, vol.106, pp.87-117, 1992.
DOI : 10.1016/0304-3975(92)90279-o
URL : https://doi.org/10.1016/0304-3975(92)90279-o
, Encompassment properties and automata with constraints, Proceedings of the 5th International Conference on Automated Deduction, vol.690, pp.328-342, 1993.
DOI : 10.1007/3-540-56868-9_25
URL : https://hal.archives-ouvertes.fr/hal-01820507
, Ground reducibility is EXPTIME-complete, Proceedings of the 12th IEEE Symposium on Logic in Computer Science, pp.26-34, 1997.
DOI : 10.1109/lics.1997.614922
URL : https://hal.archives-ouvertes.fr/inria-00072859
, Ch. 6: Rewrite Systems, Handbook of Theoretical Computer Science, vol.B, pp.244-320, 1990.
, Term Rewriting and all That, 1998.
, Rewriting, Handbook of Automated Reasoning, vol.I, pp.535-610, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01853138
, Term Rewriting Systems, vol.55, 2003.
, Well-quasi ordering, the tree theorem and Vazsonyi's conjecture, Transactions of the American Mathematical Society, vol.95, pp.210-225, 1960.
, Rewriting on ground terms, HAL-INRIA Open Archive Number, 2009.
, Completeness results for basic narrowing, Applicable Algebra in Engineering, vol.5, pp.213-253, 1994.
, Proving innermost normalisation automatically, Proceedings of the 8th Conference on Rewriting Techniques and Applications, vol.1232, pp.157-171, 1997.
DOI : 10.1007/3-540-62950-5_68
URL : https://dspace.library.uu.nl/bitstream/1874/18360/1/arts_97_proving.pdf
, Proving weak termination also provides the right way to terminate-Extended version-, HAL-INRIA Open Archive Number, 2004.
, Computing constructor forms with non terminating rewrite programs-extended version-, HAL-INRIA Open Archive Number inria-00113146, 2006.
, Modular access control via strategic rewriting, Proceedings of 12th European Symposium On Research In Computer Security, pp.578-593, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00185697
, Improving dependency pairs, Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol.2850, pp.165-179, 2003.