F. Alessi and F. Barbanera, Strong conjunction and intersection types [Agd16] The Agda Programming LanguageOnline; accessed 2-september-2016]. [Bar84] Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, MFCS Logic and the Foundations of Mathematics, pp.64-73, 1984.

H. Barendregt, M. Coppo, and M. Dezani-ciancaglini, A filter lambda model and the completeness of type assignment, BM94] Franco Barbanera and Simone Martini. Proof-functional connectives and realizability. Archive for Mathematical Logic, pp.931-940202, 1983.
DOI : 10.1002/malq.19800261902

M. Coppo and M. Dezani-ciancaglini, An extension of the basic functionality theory for the $\lambda$-calculus., Notre Dame Journal of Formal Logic, vol.21, issue.4, pp.685-693, 1980.
DOI : 10.1305/ndjfl/1093883253

M. Coppo, A. Ferrari, [. Capitani, M. Loreti, and B. Venneri, Type inference, abstract interpretation and strictness analysis [Coq16] The Coq Proof Assistant, Theoretical Computer Science Hyperformulae, Parallel Deductions and Intersection Types. BOTH, Electr. Notes Theor. Comput. Sci, vol.121, issue.502, pp.113-143180, 1993.

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.
DOI : 10.1305/ndjfl/1039724889

J. Daniel, L. Dougherty, and . Liquori, Logic and computation in a lambda calculus with intersection and union types, Logic for Programming, Artificial Intelligence, and Reasoning -16th International Conference, LPAR- 16, pp.173-191, 2010.

J. Dunfield, Elaborating intersection and union types [Epi16] The Epigram Programming Language. https://code.google.com/ archive [Online; accessed 2-september-2016]. [HHP93] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics [Idr16] The Idris Programming Language, Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, pp.17-28143, 1993.

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.
URL : https://hal.archives-ouvertes.fr/hal-01149611

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

K. Robert, R. Meyer, and . Routley, Algebraic analysis of entailment I

C. Benjamin and . Pierce, Types and Programming Languages, Pot80] Garrel Pottinger. A type assignment for the strongly normalizable ?-terms, 2002.

I. To and H. B. , Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.561-577, 1980.

D. Prawitz, Ideas and Results in Proof Theory, Proceedings of the Second Scandinavian Logic Symposium. North-Holland, 1971.
DOI : 10.1016/S0049-237X(08)70849-8

C. Benjamin, D. N. Pierce, and . Turner, Simple type-theoretic foundations for object-oriented programming, Journal of Functional Programming, vol.4, issue.2, pp.207-247, 1994.

C. John and . Reynolds, Design of the programming language Forsythe, Algol-like Languages. Birkhauser, 1996.

C. John and . Reynolds, Theories of Programming Languages Intersection typed lambda-calculus, Electr. Notes Theor. Comput. Sci, vol.70, issue.1, 1998.

J. B. Wells, A. Dimock, R. Muller, and F. Turbak, A calculus with polymorphic and polyvariant flow types, Journal of Functional Programming, vol.12, issue.03, pp.183-227, 2002.
DOI : 10.1017/S0956796801004245

J. B. Wells and C. Haack, Branching Types, Lecture Notes in Computer Science, vol.2305, pp.115-132, 2002.
DOI : 10.1007/3-540-45927-8_9