A. Aiken, Introduction to set constraint-based program analysis, Science of Computer Programming, vol.35, issue.2-3, pp.79-111, 1999.
DOI : 10.1016/S0167-6423(99)00007-6
URL : https://doi.org/10.1016/s0167-6423(99)00007-6

A. Aiken and E. L. 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://www.cs.berkeley.edu/~aiken/publications/papers/fpca93.ps

P. Henk and . Barendregt, The ?-Calculus. Studies in logic and the foundations of mathematics, 1984.

P. Henk and . Barendregt, The ?-Calculus with Types Association for Symbolic Logic, 2013.

P. Henk, M. Barendregt, M. Coppo, and . Dezani-ciancaglini, A Filter Lambda Model and the Completeness of Type Assignment, Journal of Symbolic Logic, vol.48, issue.4, pp.931-940, 1983.

K. B. Bruce, R. D. Cosmo, and G. Longo, Provable isomorphisms of types, Mathematical Structures in Computer Science, vol.19, issue.02, pp.231-247, 1992.
DOI : 10.1305/ndjfl/1093883461

. Bdcd95, M. Franco-barbanera, U. Dezani-ciancaglini, and . Liguoro, Intersection and union types: syntax and semantics, BM94. Franco Barbanera and Simone Martini. Proof-functional connectives and realizability. Archive for Mathematical Logic, pp.202-230189, 1994.

M. Flemming and . Damm, Subtyping with union types, intersection types and recursive types, TACS, pp.687-706, 1994.

D. , M. Dezani-ciancaglini, S. Ghilezan, and B. Venneri, The " relevance " of intersection and union types, Notre Dame Journal of Formal Logic, vol.38, issue.2, pp.246-269, 1997.

D. J. Dougherty, U. De-'liguoro, L. Liquori, and C. Stolze, A Realizability Interpretation for Intersection and Union Types, APLAS, pp.187-205, 2016.
DOI : 10.1007/3-540-45927-8_9
URL : https://hal.archives-ouvertes.fr/hal-01317213

J. Daniel, L. Dougherty, and . Liquori, Logic and computation in a lambda calculus with intersection and union types, LPAR, pp.173-191, 2010.

J. Dunfield and F. Pfenning, Tridirectional typechecking, POPL, pp.281-292, 2004.
DOI : 10.1145/964001.964025
URL : http://www.cs.cmu.edu/~fp/papers/popl04.pdf

J. Dunfield, Elaborating intersection and union types, Journal of Functional Programming, vol.12, issue.2-3, pp.133-165, 2014.
DOI : 10.1007/BF01211394

A. Frisch, G. Castagna, and V. Benzaken, Semantic subtyping, Journal of the ACM, vol.55, issue.4, pp.1-1964, 2008.
DOI : 10.1145/1391289.1391293
URL : https://hal.archives-ouvertes.fr/hal-00152690

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060
URL : http://www.cs.cmu.edu/~rwh/papers/lf/jacm93.ps

H. J. and R. Hindley, The simple semantics for Coppo-Dezani-Sall?? types, International Symposium on Programming, pp.212-226, 1982.
DOI : 10.1007/3-540-11494-7_15

H. A. William and . Howard, The Formulae-as-Types Notion of Construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980.

G. K. Edgar and . Lopez-escobar, Proof functional connectives, Methods in Mathematical Logic, pp.208-221, 1985.

L. Liquori and S. Rocca, Intersection typed systemàsystem`systemà la Church, Information and Computation, vol.9, issue.205, pp.1371-1386, 2007.
DOI : 10.1016/j.entcs.2005.06.015
URL : https://hal.archives-ouvertes.fr/hal-01149611

L. Liquori and C. Stolze, A Decidable Subtyping Logic for Intersection and Union Types, Research report, vol.19, issue.3, 2017.
DOI : 10.1016/S0019-9958(86)80019-5
URL : https://hal.archives-ouvertes.fr/hal-01760641

M. and G. Mints, The completeness of provable realizability., Notre Dame Journal of Formal Logic, vol.30, issue.3, pp.420-441, 1989.
DOI : 10.1305/ndjfl/1093635158

D. B. Macqueen, G. D. Plotkin, and R. Sethi, An ideal model for recursive polymorphic types, Information and Control, vol.71, issue.1-2, pp.95-130, 1986.
DOI : 10.1016/S0019-9958(86)80019-5

K. Robert, R. Meyer, and . Routley, Algebraic analysis of entailment I. Logique et Analyse Pfe93. Frank Pfenning. Refinement types for logical frameworks, TYPES, pp.407-428, 1972.

C. Benjamin and . Pierce, Programming with intersection types, union types, and bounded polymorphism, 1991.

P. Pottinger, A type assignment for the strongly normalizable ?-terms Natural deduction: a proof-theoretical study, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism Pra65. Dag Prawitz, pp.561-577, 1965.

C. John and . Reynolds, Design of the programming language Forsythe, 1996.

H. Seidl, Deciding equivalence of finite tree automata, Journal of Symbolic Logic, vol.19, issue.3, pp.424-437, 1990.