R. Alur, S. Chaudhuri, and P. Madhusudan, Visibly pushdown tree languages Available on, 2006.
DOI : 10.1145/1007352.1007390

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

R. Alur and P. Madhusudan, Visibly pushdown languages, Proceedings of the thirty-sixth annual ACM symposium on Theory of computing , STOC '04, pp.202-211, 2004.
DOI : 10.1145/1007352.1007390

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, Handbook of Automated Reasoning, 2001.
DOI : 10.1016/B978-044450813-3/50004-7

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

B. Bogaert and S. Tison, Equality and disequality constraints on direct subterms in tree automata, 9th Symp. on Theoretical Aspects of Computer Science, STACS, pp.161-171, 1992.
DOI : 10.1007/3-540-55210-3_181

J. Chabin and P. Réty, Visibly Pushdown Languages and Term Rewriting, Proc. 6th International Symposium Frontiers of Combining Systems (FroCoS), pp.252-266, 2007.
DOI : 10.1007/978-3-540-74621-8_17

URL : https://hal.archives-ouvertes.fr/inria-00462510

W. Charatonik and A. Podelski, Set constraints with intersection, Proc. IEEE Symposium on Logic in Computer Science, Varsaw, 1997.
DOI : 10.1109/lics.1997.614962

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

H. Comon and V. Cortier, Tree automata with one memory set constraints and cryptographic protocols, Theoretical Computer Science, vol.331, issue.1, pp.143-214, 2005.
DOI : 10.1016/j.tcs.2004.09.036

URL : https://hal.archives-ouvertes.fr/inria-00000553

H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez et al., Tree Automata Techniques and Applications, 1997.

H. Comon and F. Jacquemard, Ground reducibility is EXPTIME-complete. Information and Computation, pp.123-153, 2003.
DOI : 10.1109/lics.1997.614922

URL : https://hal.archives-ouvertes.fr/inria-00578859

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

N. Dershowitz and J. Jouannaud, Rewrite systems, chapter Handbook of Theoretical Computer Science, pp.243-320, 1990.

T. Frühwirth, E. Shapiro, M. Vardi, and E. Yardeni, 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. Goubault-larrecq, Résolution ordonnée avec sélection et classes décidables en logique du premier ordre, Lecture Notes, 2006.

I. Guessarian, Pushdown tree automata. Theory of Computing Systems, pp.237-263, 1983.
DOI : 10.1007/bf01744582

URL : https://hal.archives-ouvertes.fr/hal-00020941

P. Habermehl, R. Iosif, and T. Vojnar, Automata-based verification of programs with tree updates, Proc. 12th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), 2006.
URL : https://hal.archives-ouvertes.fr/hal-00150145

T. Jensen, D. L. Métayer, and T. Thorn, Verification of control flow based security policies, Proceedings of the IEEE Symposium on Research in Security and Privacy, pp.89-103, 1999.

D. Kapur, Essays in Honor of Larry Wos, chapter Constructors can be Partial Too, 1997.

J. Misra, Powerlist: a structure for parallel recursion, ACM Transactions on Programming Languages and Systems, vol.16, issue.6, pp.1737-1767, 1994.
DOI : 10.1145/197320.197356

F. Nielson, H. R. Nielson, and H. Seidl, Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi, Proc. 9th Static Analysis Symposium (SAS), volume 2477 of LNCS, pp.20-35, 2002.
DOI : 10.1007/3-540-45789-5_5

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Handbook of Automated Reasoning, 2001.
DOI : 10.1016/B978-044450813-3/50009-6

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

K. M. Schimpf and J. Gallier, Tree pushdown automata, Journal of Computer and System Sciences, vol.30, issue.1, pp.25-40, 1985.
DOI : 10.1016/0022-0000(85)90002-9

URL : http://doi.org/10.1016/0022-0000(85)90002-9