L. Afanasiev, P. Blackburn, I. Dimitriou, B. Gaiffe, E. Goris et al., PDL for ordered trees, Journal of Applied Non-Classical Logics, vol.32, issue.2, pp.115-135, 2005.
DOI : 10.3166/jancl.15.115-135
URL : https://hal.archives-ouvertes.fr/inria-00001206

P. Barceló and L. Libkin, Temporal Logics over Unranked Trees, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.31-40, 2005.
DOI : 10.1109/LICS.2005.51

M. Benedikt, W. Fan, and F. Geerts, XPath satisfiability in the presence of DTDs, PODS '05: Proceedings of the twenty-fourth ACM Symposium on Principles of Database Systems, pp.25-36, 2005.

V. Benzaken, G. Castagna, and A. Frisch, CDuce: An XMLcentric general-purpose language, ICFP '03: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pp.51-63, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00152619

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/TC.1986.1676819

J. Clark and S. Derose, XML path language (XPath) version 1.0, W3C recommendation, 1999.

D. Colazzo, G. Ghelli, P. Manghi, and C. Sartiani, Static analysis for path correctness of XML queries, Journal of Functional Programming, vol.16, issue.4&5, pp.4-5621, 2006.
DOI : 10.1017/S0956796806005983

S. Dal-zilio, D. Lugiez, and C. Meyssonnier, A logic you can count on, POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.135-146, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00071562

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

E. A. Emerson and C. S. Jutla, Tree automata, µ-calculus and determinacy, Proceedings of the 32nd annual Symposium on Foundations of Computer Science, pp.368-377, 1991.
DOI : 10.1109/sfcs.1991.185392

W. Fan, C. Chan, and M. Garofalakis, Secure XML querying with security views, Proceedings of the 2004 ACM SIGMOD international conference on Management of data , SIGMOD '04, pp.587-598, 2004.
DOI : 10.1145/1007568.1007634

V. Gapeyev and B. C. Pierce, Regular object types A preliminary version was presented at FOOL '03, European Conference on Object-Oriented Programming, 2003.

P. Genevès and N. Laya¨?dalaya¨?da, A system for the static analysis of XPath, ACM Transactions on Information Systems, vol.24, issue.4, pp.475-502, 2006.
DOI : 10.1145/1185877.1185882

P. Genevès and N. Laya¨?dalaya¨?da, Deciding XPath containement with MSO. Data & Knowledge Engineering, to appear, 2007.

P. Genevès, N. Laya¨?dalaya¨?da, and A. Schmitt, A satisfiability solver for XML and XPath, 2006.

P. Genevès and J. Vion-dury, Logic-based XPath optimization, DocEng '04: Proceedings of the 2004 ACM Symposium on Document Engineering, pp.211-219, 2004.

E. Grädel, W. Thomas, and T. Wilke, Automata logics, and infinite games: a guide to current research, 2002.
DOI : 10.1007/3-540-36387-4

H. Hosoya, J. Vouillon, and B. C. Pierce, Regular expression types for XML, ACM Transactions on Programming Languages and Systems, vol.27, issue.1, pp.46-90, 2005.
DOI : 10.1145/1053468.1053470
URL : https://hal.archives-ouvertes.fr/hal-00009271

G. P. Huet, The Zipper, Journal of Functional Programming, vol.7, issue.5, pp.549-554, 1997.
DOI : 10.1017/S0956796897002864

D. Kozen, Results on the Propositional ??-Calculus, DAIMI Report Series, vol.11, issue.146, pp.333-354, 1983.
DOI : 10.7146/dpb.v11i146.7420

M. Y. Levin and B. C. Pierce, Type-Based Optimization for Regular Patterns, DBPL '05: Proceedings of the 10th International Symposium on Database Programming Languages, 2005.
DOI : 10.1007/11601524_12

G. Miklau and D. Suciu, Containment and equivalence for a fragment of XPath, Journal of the ACM, vol.51, issue.1, pp.2-45, 2004.
DOI : 10.1145/962446.962448

A. Møller and M. I. Schwartzbach, The design space of type checkers for XML transformation languages, Proc. Tenth International Conference on Database Theory, ICDT '05, pp.17-36, 2005.

M. Murata, D. Lee, M. Mani, and K. Kawaguchi, Taxonomy of XML schema languages using formal language theory, ACM Transactions on Internet Technology, vol.5, issue.4, pp.660-704, 2005.
DOI : 10.1145/1111627.1111631

G. Pan, U. Sattler, and M. Y. Vardi, BDD-based decision procedures for the modal logic K ???, Journal of Applied Non-Classical Logics, vol.2, issue.2, pp.169-208, 2006.
DOI : 10.1016/0004-3702(92)90049-4

T. Schwentick, XPath query containment, ACM SIGMOD Record, vol.33, issue.1, pp.101-109, 2004.
DOI : 10.1145/974121.974140

Y. Tanabe, K. Takahashi, M. Yamamoto, A. Tozawa, and M. Hagiya, A decision procedure for the alternation-free two-way modal µcalculus, TABLEAUX 2005, pp.277-291, 2005.

A. Tozawa, On binary tree logic for XML and its satisfiability test, PPL '04: Informal Proceedings of the Sixth JSSST Workshop on Programming and Programming Languages, 2004.

M. Y. Vardi, Reasoning about the past with two-way automata, ICALP '98: Proceedings of the 25th International Colloquium on Automata, Languages and Programming, pp.628-641, 1998.
DOI : 10.1007/BFb0055090