A. Aiken and E. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture , FPCA '93, pp.31-41, 1993.
DOI : 10.1145/165180.165188

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

A. Aiken, E. Wimmers, and T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.163-173, 1994.
DOI : 10.1145/174675.177847

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

A. Aiken, E. Wimmers, and J. Palsberg, Optimal Representations of Polymorphic Types with Subtyping, Proceedings of 3rd International Symposium on Theoretical Aspects of Computer Software (TACS'97), pp.47-76, 1997.

R. 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

L. O. Andersen, Program Analysis and Specialization for the C Programming Language, 1994.

A. Boudet and H. Comon, Diophantine equations, Presburger arithmetic and finite automata, Proceedings of Trees in Algebra and Programming (CAAP'96), pp.30-43, 1996.
DOI : 10.1007/3-540-61064-2_27

J. Büchi, Weak second order logic and finite automata, Z. Math. Logik, Grundlag. Math, vol.5, pp.66-62, 1960.

H. Comon, SOLVING SYMBOLIC ORDERING CONSTRAINTS, International Journal of Foundations of Computer Science, vol.01, issue.04, pp.387-411, 1990.
DOI : 10.1142/S0129054190000278

H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez et al., Ordering constraints on trees, Colloquium on Trees in Algebra and Programming, pp.1-14, 1994.
DOI : 10.1007/BFb0017470

H. Comon and R. Treinen, The first-order theory of lexicographic path orderings is undecidable, Theoretical Computer Science, vol.176, issue.1-2, pp.67-87, 1997.
DOI : 10.1016/S0304-3975(96)00049-7

M. Fähndrich and A. Aiken, Making Set-Constraint Based Program Analyses Scale In First Workshop on Set Constraints at CP'96, 1996.

C. Flanagan and M. Felleisen, Componential Set-Based Analysis, Proceedings of the 1997 ACM SIGPLAN Conference on Programming Language Design and Implementation, 1997.
DOI : 10.1145/258916.258937

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

C. Flanagan, M. Flatt, S. Krishnamurthi, S. Weirich, and M. Felleisen, Catching Bugs in the Web of Program Invariants, Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.23-32, 1996.

N. Heintze, Set Based Analysis of ML Programs, Proceedings of the 1994 ACM Conference on LISP and Functional Programming, pp.306-323, 1994.

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.352-361, 1997.
DOI : 10.1109/LICS.1997.614961

F. Henglein and J. Rehof, Constraint automata and the complexity of recursive subtype entailment, Proceedings of the 25th International Colloquium on Automata , Languages, and Programming (ICALP), pp.616-627, 1998.
DOI : 10.1007/BFb0055089

D. Kozen, J. Palsberg, and M. I. Schwartzbach, Efficient Recursive Subtyping, Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.419-428, 1993.

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. J. Maher, Complete axiomatizations of the algebras of finite, rational and infinite trees, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.348-357, 1988.
DOI : 10.1109/LICS.1988.5132

S. Marlow and P. Wadler, A Practical Subtyping System For Erlang, Proceedings of the International Conference on Functional Programming (ICFP '97), pp.136-149, 1997.

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4

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

M. Müller, J. Niehren, and R. Treinen, The first-order theory of ordering constraints over feature trees, Discrete Mathematics and Theoretical Computer Science, vol.4, issue.2, pp.193-234, 2001.

J. Niehren, M. Müller, and J. Talbot, Entailment of atomic set constraints is PSPACE-complete, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.285-294, 1999.
DOI : 10.1109/LICS.1999.782623

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

J. Niehren and T. Priesnitz, Entailment of Non-structural Subtype Constraints, Asian Computing Science Conference, number 1742 in LNCS, 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, Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS'01), number 2215 in LNCS, pp.360-384, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00536514

M. Odersky and P. Wadler, Pizza into Java, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.146-159, 1997.
DOI : 10.1145/263699.263715

J. Palsberg and P. O. Keefe, A type system equivalent to flow analysis, ACM Transactions on Programming Languages and Systems, vol.17, issue.4, pp.576-599, 1995.
DOI : 10.1145/210184.210187

J. Palsberg and M. I. Schwartzbach, Object-Oriented Type Inference, Proceedings of the ACM Conference on Object-Oriented programming: Systems, Languages, and Applications, pp.146-161, 1991.

E. L. Post, A Variant of a Recursively Unsolvable Problem . Bull. of the Am, Math. Soc, vol.52, 1946.

F. Pottier, Simplifying Subtyping Constraints, Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP '96), 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, Simplifying Subtyping Constraints: A Theory, Information and Computation, vol.170, issue.2, 2000.
DOI : 10.1006/inco.2001.2963

M. O. Rabin, Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the, pp.1-35, 1969.

J. Rehof, The Complexity of Simple Subtyping Systems, 1998.

O. Shivers, Control Flow Analysis in Scheme, Proceedings of the 1988 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.164-174, 1988.

B. Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.32-41, 1996.
DOI : 10.1145/237721.237727

Z. Su and A. Aiken, Entailment with Conditional Equality Constraints, Proceedings of European Symposium on Programming, pp.170-189, 2001.
DOI : 10.1007/3-540-45309-1_12

R. Treinen, A new method for undecidability proofs of first order theories, Journal of Symbolic Computation, vol.14, issue.5, pp.437-457, 1992.
DOI : 10.1016/0747-7171(92)90016-W

R. Treinen, Predicate Logic and Tree Automata with Tests, Foundations of Software Science and Computation Structures, volume LNCS 1784, pp.329-343, 2000.
DOI : 10.1007/3-540-46432-8_22

V. Trifonov and S. Smith, Subtyping constrained types, Proceedings of the 3rd International Static Analysis Symposium, 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

K. N. Venkataraman, Decidability of the purely existential fragment of the theory of term algebras, Journal of the ACM, vol.34, issue.2, pp.492-510, 1987.
DOI : 10.1145/23005.24037

P. Wolper and B. Boigelot, An automata-theoretic approach to Presburger arithmetic constraints, Static Analysis Symposium, pp.21-32, 1995.
DOI : 10.1007/3-540-60360-3_30