S. Boag, D. Chamberlin, M. Fernández, D. Florescu, J. Robie et al., XQuery 1.0: An XML Query Language, 2010.

H. Hosoya, J. Vouillon, and B. C. Pierce, Regular expression types for XML, ACM Trans. Program. Lang. Syst, vol.27, issue.1, pp.46-90, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00009271

D. Draper, M. Dyck, P. Fankhauser, M. Fernández, A. Malhotra et al., , 2010.

J. Clark and S. Derose, XML Path Language (XPath) Version 1.0, W3C Recommendation, 1999.

A. Berglund, S. Boag, D. Chamberlin, M. F. Fernández, M. Kay et al., XML Path Language (XPath) 2.0, second edition, W3C Recommendation, 2010.

J. Robie, D. Chamberlin, M. Dyck, and J. Snelson, XML Path Language (XPath) 3.0, W3C Recommendation, 2014.

J. Robie, D. Chamberlin, M. Dyck, and J. Snelson, XQuery 3.0: An XML Query Language, W3C Recommendation, 2014.

D. Colazzo and C. Sartiani, Precision and complexity of XQuery type inference, Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming, pp.89-100, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00626217

A. Tozawa, Towards static type checking for XSLT, ACM Symposium on Document Engineering, pp.18-27, 2001.

T. Milo, D. Suciu, and V. Vianu, Typechecking for XML transformers, J. Comput. Syst. Sci, vol.66, issue.1, pp.30-32, 2003.

T. Perst and H. Seidl, Macro forest transducers, Inf. Process. Lett, vol.89, issue.3, pp.141-149, 2004.

S. Maneth, A. Berlea, T. Perst, and H. Seidl, XML type checking with macro tree transducers, Proceedings of the Twenty-Fourth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS '05, pp.283-294, 2005.

A. Tozawa, XML type checking using high-level tree transducer, Proceedings of the 8th International Symposium on Functional and Logic Programming, FLOPS '06, pp.81-96, 2006.

A. Frisch and H. Hosoya, Towards practical typechecking for macro tree transducers, Proceedings of the 11th International Conference on Database Programming Languages, DBPL'07, pp.246-260, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00126895

J. Engelfriet and H. Vogler, Macro tree transducers, J. Comput. Syst. Sci, vol.31, issue.1, pp.90066-90068, 1985.

J. Engelfriet, The time complexity of typechecking tree-walking tree transducers, Acta Inform, vol.46, issue.2, pp.139-154, 2009.

G. Castagna, H. Im, K. Nguyen, and V. Benzaken, A core calculus for XQuery 3.0: combining navigational and pattern matching approaches, Proceedings of the 24th European Symposium on Programming, pp.232-256, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01104872

G. Huet, The zipper, J. Funct. Program, vol.7, issue.5, pp.549-554, 1997.

P. Genevès and N. Gesbert, XQuery and static typing: tackling the problem of backward axes, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, pp.88-100, 2015.

P. Genevès, N. Layaïda, and A. Schmitt, Efficient static analysis of XML paths and types, Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '07, pp.342-351, 2007.

S. Maneth, T. Perst, and H. Seidl, Exact XML type checking in polynomial time, Proceedings of the 11th International Conference on Database Theory, ICDT'07, pp.254-268, 2006.

N. Kobayashi, N. Tabuchi, and H. Unno, Higher-order multi-parameter tree transducers and recursion schemes for program verification, Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '10, pp.495-508, 2010.

N. Alon, T. Milo, F. Neven, D. Suciu, and V. Vianu, XML with data values: typechecking revisited, J. Comput. Syst. Sci, vol.66, issue.4, pp.32-33, 2003.

H. Hosoya and B. C. Pierce, XDuce: a statically typed XML processing language, ACM Trans. Internet Technol, vol.3, issue.2, pp.117-148, 2003.

M. Murata, D. Lee, M. Mani, and K. Kawaguchi, Taxonomy of XML schema languages using formal language theory, ACM Trans. Internet Technol, vol.5, issue.4, pp.660-704, 2005.

R. M. Amadio and L. Cardelli, Subtyping recursive types, ACM Trans. Program. Lang. Syst, vol.15, issue.4, pp.575-631, 1993.
URL : https://hal.archives-ouvertes.fr/inria-00070035

A. Brüggemann-klein and D. Wood, One-unambiguous regular languages, Inf. Comput, vol.140, issue.2, pp.229-253, 1998.

P. Genevès, N. Layaïda, A. Schmitt, and N. Gesbert, Efficiently deciding ?-calculus with converse over finite trees, ACM Trans. Comput. Log, vol.16, issue.2, p.16, 2015.

M. Wand, A simple algorithm and proof for type inference, Fundam. Inform, vol.10, pp.115-122, 1987.

F. Pottier, Simplifying subtyping constraints: a theory, Inf. Comput, vol.170, issue.2, pp.153-183, 2001.

G. M. Bierman, A. D. Gordon, C. Hri¸tcu, and D. Langworthy, Semantic subtyping with an SMT solver, J. Funct. Program, vol.22, issue.1, pp.31-105, 2012.

A. Frisch, G. Castagna, and V. Benzaken, Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types, J. ACM, vol.55, issue.4, p.19, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00336120

S. Heubach and T. Mansour, Combinatorics of Compositions and Words, 2009.

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

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

V. Benzaken, G. Castagna, H. Hosoya, B. C. Pierce, and S. Vansummeren, Encyclopedia of Database Systems, pp.3646-3650, 2009.

S. Hakuta, S. Maneth, K. Nakano, and H. Iwasaki, IEEE 30th International Conference on Data Engineering, ICDE '14, pp.952-963, 2014.

A. Aho and J. Ullman, Translations on a context free grammar, Inf. Control, vol.19, issue.5, pp.90706-90712, 1971.

D. Olteanu, H. Meuss, T. Furche, and F. Bry, XML-Based Data Management and Multimedia Engineering -EDBT, pp.109-127, 2002.

D. Olteanu, Forward node-selecting queries over trees, ACM Trans. Database Syst, vol.32, issue.1, 2007.

A. Møller, M. O. Olesen, and M. I. Schwartzbach, Static validation of XSL transformations, ACM Trans. Program. Lang. Syst, vol.29, issue.4, 2007.

J. Clark, XSL Transformations (XSLT) Version 1.0, W3C Recommendation, 1999.

V. Benzaken, G. Castagna, D. Colazzo, and K. Nguyen, Optimizing XML querying using type-based document projection, ACM Trans. Database Syst, vol.38, issue.1, p.4, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00798049

M. Benedikt and J. Cheney, Semantics, types and effects for XML updates, Proceedings of the 12th International Symposium on Database Programming Languages, DBPL '09, pp.1-17, 2009.

J. Robie, D. Chamberlin, M. Dyck, D. Florescu, J. Melton et al., XQuery Update Facility 1.0, W3C Recommendation, 2011.

M. Benedikt and J. Cheney, Destabilizers and independence of XML updates, Proc. VLDB Endow. 3 (1-2), pp.906-917, 2010.

N. Klarlund and A. Møller, MONA Version 1.4 User Manual, BRICS, 2001.

P. Genevès and N. Layaïda, Deciding XPath containment with MSO, Data Knowl. Eng, vol.63, issue.1, pp.108-136, 2007.

J. Doner, Tree acceptors and some of their applications, J. Comput. Syst. Sci, vol.4, issue.5, pp.80041-80042, 1970.

N. Kobayashi, Model-checking higher-order functions, Proceedings of the 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP '09, pp.25-36, 2009.

M. Benedikt and H. Vu, Proceedings of the 15th International Workshop on the Web and Databases, pp.43-48, 2012.

N. Gesbert, P. Genevès, and N. Layaïda, Parametric polymorphism and semantic subtyping: the logical connection, Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, pp.107-116, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00585686