H. Bar91 and . Barendregt, Introduction to generalized type systems, Journal of Functional Programming, vol.1, issue.2, pp.125-154, 1991.

H. Barendregt, M. Coppo, and M. Dezani-ciancaglini, A filter lambda model and the completeness of type assignment, The Journal of Symbolic Logic, vol.37, issue.04, pp.931-940, 1983.
DOI : 10.1002/malq.19800261902

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

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.

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://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.5854

H. F. Honsell, L. Liquori, I. Scagnetto, and S. Claude, The strong logical framework and bull, its incarnation. Manuscript, work in progress, Inria, pp.2017-2024

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 https, 2017.

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, pp.407-428, 1972.

P. Pottinger, A type assignment for the strongly normalizable ?-terms, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.561-577, 1980.