M. Abadi and V. Cortier, Deciding knowledge in security protocols under equational theories, Theoretical Computer Science, vol.367, issue.1-2, pp.2-32, 2006.
DOI : 10.1016/j.tcs.2006.08.032
URL : https://hal.archives-ouvertes.fr/inria-00000554

M. Abadi and C. Fournet, Mobile values, new names, and secure communication, POPL'01
URL : https://hal.archives-ouvertes.fr/hal-01423924

F. Baader and W. Snyder, Unification theory In Handbook of Automated Reasoning, volume I, chapter 8, pp.445-532, 2001.

A. Blumensath and E. Grädel, Automatic structures, Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), pp.51-62, 2000.
DOI : 10.1109/LICS.2000.855755

A. Caron, J. Coquide, and M. Dauchet, Encompassment properties and automata with constraints, RTA, pp.328-342, 1993.
DOI : 10.1007/3-540-56868-9_25

H. Comon, SOLVING SYMBOLIC ORDERING CONSTRAINTS, International Journal of Foundations of Computer Science, vol.01, issue.04, pp.387-412, 1990.
DOI : 10.1142/S0129054190000278

H. Comon and C. Delor, Equational Formulas with Membership Constraints, Information and Computation, vol.112, issue.2, pp.167-216, 1994.
DOI : 10.1006/inco.1994.1056

H. Comon, M. Haberstrau, and J. Jouannaud, Syntacticness, Cycle-Syntacticness, and Shallow Theories, Information and Computation, vol.111, issue.1, pp.154-191, 1994.
DOI : 10.1006/inco.1994.1043
URL : http://doi.org/10.1006/inco.1994.1043

H. Comon and P. Lescanne, Equational problems anddisunification, Journal of Symbolic Computation, vol.7, issue.3-4, pp.371-425, 1989.
DOI : 10.1016/S0747-7171(89)80017-3

M. Dauchet, S. Tison, T. Heuillard, and P. Lescanne, Decidability of confluence for ground term rewriting systems, LICS, pp.353-359, 1987.
DOI : 10.1007/BFb0028794

M. Dauchet, S. Tison, T. Heuillard, and P. Lescanne, Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems, Information and Computation, vol.88, issue.2, pp.187-201, 1990.
DOI : 10.1016/0890-5401(90)90015-A

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230

H. Hüttel and M. D. Pedersen, A Logical Characterisation of Static Equivalence, Electronic Notes in Theoretical Computer Science, vol.173, pp.139-157, 2007.
DOI : 10.1016/j.entcs.2007.02.032

J. Jouannaud and M. Okada, Satisfiability of systems of ordinal notations with the subterm property is decidable, ICALP, pp.455-468, 1991.
DOI : 10.1007/3-540-54233-7_155

V. Kuncak and M. C. Rinard, Structural subtyping of non-recursive types is decidable 17. ´ E. Lozes and J. Villard. A spatial equational logic for the applied ?-calculus, Logic in Computer Science 18. ´ E. Lozes and J. Villard. A spatial equational logic for the applied ?-calculus. Distributed Computing, pp.96-107, 2003.

M. J. Maher, Complete axiomatizations of the algebras of finite, rational and infinite trees, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.348-357, 1988.
DOI : 10.1109/LICS.1988.5132

A. I. Malc-'ev, Axiomatizable classes of locally free algebras of various type, The Metamathematics of Algebraic Systems: Collected Papers, 1936.

J. Marcinkowski, Undecidability of the ? * ? * part of the theory of ground term algebra modulo an AC symbol, RTA, pp.92-102, 1999.

Z. Su, A. Aiken, J. Niehren, T. Priesnitz, and R. Treinen, The first-order theory of subtyping constraints, POPL, pp.203-216, 2002.

R. Treinen, A new method for undecidability proofs of first order theories, Journal of Symbolic Computation, vol.14, issue.5, pp.437-457, 1992.
DOI : 10.1016/0747-7171(92)90016-W