J. Coquidé, M. Dauchet, R. Gilleron, and S. Vágvölgyi, Bottom-up tree pushdown automata: classification and connection with rewrite systems, Theoretical Computer Science, vol.127, issue.1, pp.69-98, 1994.
DOI : 10.1016/0304-3975(94)90101-5

J. Coquidé and R. Gilleron, Proofs and reachability problem for ground rewrite systems, Proc. of the 6th International Meeting of Young Computer Scientists, pp.120-129, 1990.
DOI : 10.1007/3-540-53414-8_34

V. Cortier, Pspace-completeness of monadic simultaneous rigid reachability, 1998.

M. Dauchet, Rewriting and tree automata, Lecture Notes in Computer Science, vol.909, pp.95-113, 1993.
DOI : 10.1007/3-540-59340-3_8

M. Dauchet, T. Heuillard, P. Lescanne, and S. Tison, The confluence of ground term rewriting systems is decidable, Proc. 3rd IEEE Symp. Logic in Computer Science, 1988.

A. Degtyarev and A. Voronkov, Simultaneous rigid E-unification is undecidable, 1995.
DOI : 10.1007/3-540-61377-3_38

A. Degtyarev, Y. Gurevich, P. Narendran, M. Veanes, and A. Voronkov, The decidability of simultaneous rigid E-unification with one variable, Lecture Notes in Computer Science, vol.1379, pp.181-195, 1998.
DOI : 10.1007/BFb0052370

N. Dershowitz and J. Jouannaud, Rewrite systemsHandbook of Theoretical Computer Science, Formal Methods and Semantics, pp.243-309, 1990.

J. Doner, Tree acceptors and some of their applications, Journal of Computer and System Sciences, vol.4, issue.5, pp.406-451, 1970.
DOI : 10.1016/S0022-0000(70)80041-1

W. Farmer, Simple second-order languages for which unification is undecidable, Theoretical Computer Science, vol.87, issue.1, pp.25-41, 1991.
DOI : 10.1016/S0304-3975(06)80003-4

T. Frühwirth, E. Shapiro, M. Y. Vardi, and E. Yardemi, Logic programs as types for logic programs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.300-309, 1991.
DOI : 10.1109/LICS.1991.151654

J. Gallier, P. Narendran, D. Plaisted, and W. Snyder, Rigid Eunification is NP-complete, Proc. IEEE Conference on Logic in Computer Science (LICS), pp.338-346, 1988.
DOI : 10.1109/lics.1988.5121

J. Gallier, S. Raatz, and W. Snyder, Theorem proving using rigid Eunification: Equational matings, Proc. IEEE Conference on Logic in Computer Science (LICS), pp.338-346, 1987.
DOI : 10.1145/128749.128754
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.500.9730

W. Goldfarb, The undecidability of the second-order unification problem, Theoretical Computer Science, vol.13, issue.2, pp.225-230, 1981.
DOI : 10.1016/0304-3975(81)90040-2

Y. Gurevich and M. Veanes, Partisan corroboration, and shifted pairing , Research Report MPI-I-98-2-014, 1998.
DOI : 10.1006/inco.1999.2797
URL : http://doi.org/10.1006/inco.1999.2797

Y. Gurevich and A. Voronkov, Monadic simultaneous rigid E-unification and related problems, Automata, Languages and Programming , 24th International Colloquium, ICALP'97, pp.154-165, 1997.
DOI : 10.1007/3-540-63165-8_173
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.9742

D. Kozen, Complexity of finitely presented algebras, Proceedings of the ninth annual ACM symposium on Theory of computing , STOC '77, pp.164-177, 1977.
DOI : 10.1145/800105.803406

J. Levy, Decidable and undecidable second-order unification problems, 9th International Conference, RTA-98, pp.47-60, 1998.
DOI : 10.1007/BFb0052360
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.157.7140

J. Levy and M. Veanes, On the undecidability of second-order unification , Invited paper for a special issue of Information and Computation on term rewriting, 1998.

H. Seidl, Haskell overloading is DEXPTIME-complete, Information Processing Letters, vol.52, issue.2, pp.57-60, 1994.
DOI : 10.1016/0020-0190(94)00130-8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.119.8086

J. Thatcher and J. Wright, Generalized finite automata theory with an application to a decision problem of second-order logic, Mathematical Systems Theory, vol.12, issue.1, pp.57-81, 1968.
DOI : 10.1007/BF01691346

M. Veanes, On computational complexity of basic decision problems of finite tree automata, 1997.

M. Veanes, The relation between second-order unification and simultaneous rigid E-unification, Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226), pp.264-275, 1998.
DOI : 10.1109/LICS.1998.705663