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. ,
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
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
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. ,
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
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. ,
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. ,
Proof functional connectives, Methods in Mathematical Logic, pp.208-221, 1985. ,
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
The completeness of provable realizability., Notre Dame Journal of Formal Logic, vol.30, issue.3, pp.420-44195, 1986. ,
DOI : 10.1305/ndjfl/1093635158
Algebraic analysis of entailment I ,
Types and Programming Languages, Pot80] Garrel Pottinger. A type assignment for the strongly normalizable ?-terms, 2002. ,
Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.561-577, 1980. ,
Ideas and Results in Proof Theory, Proceedings of the Second Scandinavian Logic Symposium. North-Holland, 1971. ,
DOI : 10.1016/S0049-237X(08)70849-8
Simple type-theoretic foundations for object-oriented programming, Journal of Functional Programming, vol.4, issue.2, pp.207-247, 1994. ,
Design of the programming language Forsythe, Algol-like Languages. Birkhauser, 1996. ,
Theories of Programming Languages Intersection typed lambda-calculus, Electr. Notes Theor. Comput. Sci, vol.70, issue.1, 1998. ,
A calculus with polymorphic and polyvariant flow types, Journal of Functional Programming, vol.12, issue.03, pp.183-227, 2002. ,
DOI : 10.1017/S0956796801004245
Branching Types, Lecture Notes in Computer Science, vol.2305, pp.115-132, 2002. ,
DOI : 10.1007/3-540-45927-8_9