R. M. Amadio and L. Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems, vol.15, issue.4, pp.575-631, 1993.
DOI : 10.1145/155183.155231
URL : https://hal.archives-ouvertes.fr/inria-00070035

M. Ben-ari, J. Y. Halpern, and A. Pnueli, Deterministic propositional dynamic logic: Finite models, complexity, and completeness, Journal of Computer and System Sciences, vol.25, issue.3, pp.402-417, 1982.
DOI : 10.1016/0022-0000(82)90018-6

P. Blackburn, B. Gaiffe, and M. Marx, Variable free reasoning on finite trees, Proceedings of Mathematics of Language, pp.17-30, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099716

P. Blackburn and W. Meyer, Linguistics, Logic and Finite Trees, Logic Journal of IGPL, vol.2, issue.1, pp.3-29, 1994.
DOI : 10.1093/jigpal/2.1.3

J. Eifrig, S. Smith, and V. Trifonov, Sound polymorphic type inference for objects, OOPSLA, pp.169-184, 1995.

M. J. Fischer and R. E. Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.2, pp.194-211, 1979.
DOI : 10.1016/0022-0000(79)90046-1

C. Flanagan and M. Felleisen, Componential set-based analysis, ACM Transactions on Programming Languages and Systems, vol.21, issue.2, pp.370-416, 1999.
DOI : 10.1145/316686.316703

A. Frey, Satisfying subtype inequalities in polynomial space, Theoretical Computer Science, vol.277, issue.1-2, pp.105-117, 2002.
DOI : 10.1016/S0304-3975(00)00314-5

Y. Fuh and P. Mishra, Type inference with subtypes, Theoretical Computer Science, vol.73, issue.2, pp.155-175, 1990.
DOI : 10.1016/0304-3975(90)90144-7

D. Harel, D. Kozen, and J. Tiuryn, Dynamic Logic, 2000.

F. Henglein and J. Rehof, The complexity of subtype entailment for simple types, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pp.362-372, 1997.
DOI : 10.1109/LICS.1997.614961

F. Henglein and J. Rehof, Constraint automata and the complexity of recursive subtype entailment, ICALP, pp.616-627, 1998.
DOI : 10.1007/BFb0055089

M. Hoang and J. Mitchell, Lower bounds on type inference with subtypes, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '95, pp.176-185, 1995.
DOI : 10.1145/199448.199481

D. Kozen, J. Palsberg, and M. I. Schwartzbach, Efficient inference of partial types, Journal of Computer and System Sciences, vol.49, issue.2, pp.306-324, 1994.
DOI : 10.1016/S0022-0000(05)80051-0

M. Kracht, Inessential features, Logical Aspects of Computational Linguistics, pp.43-62, 1997.
DOI : 10.1007/BFb0052150

V. Kuncak and M. Rinard, Structural subtyping of non-recursive types is decidable, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.96-107, 2003.
DOI : 10.1109/LICS.2003.1210049

J. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '84, pp.175-185, 1984.
DOI : 10.1145/800017.800529

J. C. Mitchell, Abstract, Journal of Functional Programming, vol.17, issue.03, pp.245-285, 1991.
DOI : 10.1016/S0019-9958(82)80087-9

J. Niehren and T. Priesnitz, Entailment of Non-structural Subtype Constraints, Asian Computing Science Conference, pp.251-265, 1999.
DOI : 10.1007/3-540-46674-6_22
URL : https://hal.archives-ouvertes.fr/inria-00536825

J. Niehren and T. Priesnitz, Non-structural subtype entailment in automata theory, Information and Computation, vol.186, issue.2, pp.319-354, 2003.
DOI : 10.1016/S0890-5401(03)00140-8
URL : https://hal.archives-ouvertes.fr/inria-00536514

J. Niehren, T. Priesnitz, and Z. Su, Complexity of Subtype Satisfiability over Posets, 2004.
DOI : 10.1007/978-3-540-31987-0_25
URL : https://hal.archives-ouvertes.fr/inria-00536523

A. Palm, Propositional tense logic for trees, Proceedings of the Sixth Meeting on Mathematics of Language, pp.74-87, 1999.

J. Palsberg, M. Wand, and P. O. Keefe, Type inference with non-structural subtyping, Formal Aspects of Computing, vol.5, issue.3, pp.49-67, 1997.
DOI : 10.1007/BF01212524
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.3123

F. Pottier, Simplifying subtyping constraints, ICFP, pp.122-133, 1996.
DOI : 10.1145/232627.232642
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7032

F. Pottier, Type inference in the presence of subtyping: from theory to practice, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00073205

V. Pratt and J. Tiuryn, Satisfiability of inequalities in a poset, Fundamenta Informaticae, vol.28, pp.165-182, 1996.

M. O. Rabin, Decidability of second-order theories and automata on infinte trees, Trans. Amer. Math. Soc, vol.141, pp.1-35, 1969.

J. Rehof, The Complexity of Simple Subtyping Systems, 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

E. Spaan, Complexity of Modal Logics, 1993.

Z. Su, A. Aiken, J. Niehren, T. Priesnitz, and R. Treinen, First-order theory of subtyping constraints, POPL, pp.203-216, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00536828

J. Tiuryn, Subtype inequalities, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.308-315, 1992.
DOI : 10.1109/LICS.1992.185543

J. Tiuryn and M. Wand, Type reconstruction with recursive types and atomic subtyping, Theory and Practice of Software Development, pp.686-70193
DOI : 10.1007/3-540-56610-4_98

V. Trifonov and S. Smith, Subtyping constrained types, SAS, pp.349-365, 1996.
DOI : 10.1007/3-540-61739-6_52
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.5192

M. Y. Vardi and P. Wolper, Automata-theoretic techniques for modal logics of programs, Journal of Computer and System Sciences, vol.32, issue.2, pp.183-221, 1986.
DOI : 10.1016/0022-0000(86)90026-7