F. Alessi, F. Barbanera, M. Dezani-ciancagliniabr93, and ]. S. Abramsky, Intersection types and lambda models, Theoretical Computer Science, vol.355, issue.2, pp.108-126, 1993.
DOI : 10.1016/j.tcs.2006.01.004
URL : http://doi.org/10.1016/j.tcs.2006.01.004

A. , R. Amadio, and P. Curien, Domains and lambda-calculi, 1998.
DOI : 10.1017/cbo9780511983504
URL : https://hal.archives-ouvertes.fr/inria-00070008

]. P. Bai02 and . Baillot, Checking polynomial time complexity with types, IFIP TCS of IFIP Conference Proceedings, pp.370-382, 2002.

]. H. Bar84 and . Barendregt, The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics, p.9, 1984.

N. Benton, G. Bierman, V. De-paiva, and M. Hyland, A term calculus for Intuitionistic Linear Logic, Proc. of the 1st Int. Conf. on Typed Lambda Calculus and Applications, pp.75-90
DOI : 10.1007/BFb0037099
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.8467

Z. Benaissa, D. Briaud, P. Lescanne, and J. , Abstract, Journal of Functional Programming, vol.1, issue.05, pp.699-722, 1996.
DOI : 10.1145/174675.174707

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

P. [. Boudol, C. Curien, and . Lavatelli, A semantics for lambda calculi with resources, Mathematical Structures in Computer Science, vol.9, issue.4, pp.437-482, 1999.
DOI : 10.1017/S0960129599002893

]. A. Bec01 and . Beckmann, Exact bounds for lengths of reductions in typed lambda-calculus, J. of Symbolic Logic, vol.66, issue.3, pp.1277-1285, 2001.

T. [. Bucciarelli, G. Ehrhard, and . Manzonetto, Categorical Models for Simply Typed Resource Calculi, Electronic Notes in Theoretical Computer Science, vol.265, issue.3, pp.213-230, 2010.
DOI : 10.1016/j.entcs.2010.08.013
URL : https://hal.archives-ouvertes.fr/hal-00527229

T. [. Blute, C. Ehrhard, and . Tasson, A convenient differential category. CoRR, abs/1006, p.3140, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00492424

G. Boudol and C. Lavatelli, Full abstraction for lambda calculus with resources and convergence testing, Trees in Algebra and Programming, 21st Int. Colloquium (CAAP'96), pp.302-316, 1996.
DOI : 10.1007/3-540-61064-2_45

]. A. Bl11a, S. Bernadet, ]. Lengrandbl11b, S. Bernadet, and . Lengrand, Complexity of strongly normalising ?-terms via nonidempotent intersection types Filter models: non-idempotent intersection types, orthogonality and polymorphism, Proc. of the 14th Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS'11) Proc. of the 20th Annual Conf. of the European Association for Computer Science Logic (CSL'11), LIPIcs. Schloss Dagstuhl LCI Mogbil. Soft lambda-calculus: a language for polynomial time computation. CoRR, cs.LO/0312015, pp.13-31, 2003.

]. C. Böh68, I. Böhm, R. Bloo, and K. H. Rose, Alcune proprietà delle forme ?-?-normali nel ?K-calcolo Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection, Computing Science in the Netherlands (CSN '95), pp.25-62, 1968.

M. [. Coppo and . Dezani-ciancaglini, A new type assignment for ??-terms, Archiv f??r Mathematische Logik und Grundlagenforschung, vol.5, issue.1, pp.139-156, 1978.
DOI : 10.1007/BF02011875
URL : http://www.digizeitschriften.de/download/PPN379931524_0019/PPN379931524_0019___log16.pdf

M. [. Coppo, P. Dezani, and . Sallé, Functional characterization of some semantic equalities inside ??-calculus, Proc. of the 6th Intern, pp.133-146
DOI : 10.1007/3-540-09510-1_11

A. [. Coquand and . Spiwack, A proof of strong normalisation using domain theory. Logic. Methods Comput, [dC05] D. de Carvalho. Intersection types for light affine lambda calculus. ENTCS, pp.31133-152, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00432490

]. D. De-carvalho, Execution time of lambda-terms via denotational semantics and intersection types, p.4251, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00319822

M. Dezani-ciancaglini, S. Ghilezan, and S. Likavec, Behavioural Inverse Limit Models, Theoret. Comput. Sci, vol.316, issue.2, pp.1-349, 2004.
DOI : 10.1016/j.tcs.2004.01.023
URL : http://doi.org/10.1016/j.tcs.2004.01.023

M. Dezani-ciancaglini, F. Honsell, and Y. Motohama, Compositional characterisations of <mml:math altimg="si1.gif" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi>??</mml:mi></mml:math>-terms using intersection types, Theoretical Computer Science, vol.340, issue.3, pp.459-495, 2005.
DOI : 10.1016/j.tcs.2005.03.011

P. [. Dougherty and . Lescanne, Reductions, intersection types, and explicit substitutions, Mathematical Structures in Computer Science, vol.13, issue.1, pp.55-85, 2003.
DOI : 10.1017/S0960129502003821

L. [. Ehrhard and . Regnier, The differential lambda-calculus, Theoretical Computer Science, vol.309, issue.1-3, pp.1-41, 2003.
DOI : 10.1016/S0304-3975(03)00392-X
URL : https://hal.archives-ouvertes.fr/hal-00150572

J. Gallier, Typing untyped ??-terms, or reducibility strikes again!, Annals of Pure and Applied Logic, vol.91, issue.2-3, pp.231-270, 1998.
DOI : 10.1016/S0168-0072(97)00047-X
URL : http://doi.org/10.1016/s0168-0072(97)00047-x

]. S. Ghi96 and . Ghilezan, Strong normalization and typability with intersection types, Notre Dame J. Formal Loigc, vol.37, issue.1 2, pp.44-52, 1996.

J. [. Ghilezan, P. Ivetic, S. Lescanne, and . Likavec, Intersection Types for the Resource Control Lambda Calculi, Proc. of the 8th Int. Colloquium on Theoretical Aspects of Computing, pp.116-134, 2011.
DOI : 10.1016/0304-3975(92)90297-S
URL : https://hal.archives-ouvertes.fr/ensl-00654755

G. Girard, Linear logic, Thèse d'´ etat Gaboardi and S. R. D. Rocca. A soft type assignment system for lambda -calculus, pp.1-101, 1972.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

]. W. How80 and . Howard, The formulae-as-types notion of construction

. Hindley and H. B. To, Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.479-490, 1969.

]. D. Kes07 and . Kesner, The theory of calculi with explicit substitutions revisited A theory of explicit substitutions with safe and full composition. Logic, Proc. of the 16th Annual Conf. of the European Association for Computer Science Logic, pp.238-252, 2007.

S. [. Kesner and . Lengrand, Extending the Explicit Substitution Paradigm, Proc. of the 16th Int. Conf. on Rewriting Techniques and Applications(RTA'05), pp.407-422, 2005.
DOI : 10.1007/978-3-540-32033-3_30
URL : https://hal.archives-ouvertes.fr/hal-00148847

S. [. Kesner, ]. Lengrand, F. Kesner, and . Renaud, Resource operators for ??-calculus, Krivine. Lambda-calcul Types et modèles, pp.419-473, 1990.
DOI : 10.1016/j.ic.2006.08.008
URL : https://hal.archives-ouvertes.fr/hal-00148539

]. Kri01 and . Krivine, Typed lambda-calculus in classical Zermelo-Fraenkel set theory, Arch. Math. Log, vol.40, issue.4, pp.189-205, 2001.

J. [. Kfoury and . Wells, Principality and decidable type inference for finiterank intersection types, Proc. of the 26th Annual ACM Symp. on Principles of Programming Languages (POPL'99), pp.161-174, 1999.
DOI : 10.1145/292540.292556
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.4246

]. D. Lei86 and . Leivant, Typing and computational properties of lambda expressions, Theoret. Comput. Sci, vol.44, issue.1, pp.51-68, 1986.

L. Lengrand, P. Lescanne, D. Dougherty, M. Dezani-ciancaglini, and S. Van-bakel, Intersection types for explicit substitutions, Information and Computation, vol.189, issue.1, pp.17-42, 2004.
DOI : 10.1016/j.ic.2003.09.004
URL : https://hal.archives-ouvertes.fr/hal-00150285

S. Lengrand and A. Miquel, Classical F ? , orthogonality and symmetric candidates
URL : https://hal.archives-ouvertes.fr/hal-00150283

A. , P. Appl, and . Logic, Mellì es. Typed ?-calculi with explicit substitution may not terminate, Proc. of the 2nd Int. Conf. on Typed Lambda Calculus and Applications (TLCA'95), pp.3-20, 2008.

. [. Munch-maccagnoni, Focalisation and classical realisabilityMellì es and J. Vouillon. Recursive polymorphic types and parametricity in an operational framework, Proc. of the 18th Annual Conf. of the European Association for Computer Science Logic 20th Annual IEEE Symp. on Logic in Computer Science, pp.409-423, 2005.
DOI : 10.1007/978-3-642-04027-6_30
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.402.5477

H. [. Neergaard and . Mairson, Types, potency, and idempotency: why nonlinearity and amnesia make a type system work, Proc. of the 9th ACM Intern. Conf. on Functional Programming, pp.138-149, 2004.
DOI : 10.1145/1016850.1016871

]. M. Par97 and . Parigot, Proofs of strong normalisation for second order classical natural deduction

]. F. Renaud, Les ressources explicites vues par la théorie de la réécriture Complexity of normalization in the pure typed lambda calculus, J. of Symbolic Logic The L. E. J. Brouwer Centenary Symposium. North-Holland, pp.1461-1479, 1982.

]. W. Tai75, S. Tait, and . Van-bakel, A realizability interpretation of the theory of species Complete restrictions of the Intersection Type Discipline, Logic Colloquium, pp.240-251, 1975.

]. S. Van-bakel, Intersection type assignment systems, Theoretical Computer Science, vol.151, issue.2, pp.385-435, 1995.
DOI : 10.1016/0304-3975(95)00073-6

F. Van-raamsdonk, P. Severi, M. H. Sørensen, and H. Xi, Perpetual Reductions in??-Calculus, Information and Computation, vol.149, issue.2, pp.173-225, 1999.
DOI : 10.1006/inco.1998.2750

F. If, then there exists ? ? ? such that ? ? ? ? ?? x : F , so ? = (x : F ) so F ? ?(x)

. Conversely, then (x : F ) ? ? and x : F ? ? ? ?? x : F

F. ?. Let and . Hence, There exists ? ? ? such that there exist ? 1 , ? 2 and A such that ? 1

F. ?. Conversely and A. , There exists A such that So there exists ? ? ? such that ? ? ? ? ?? M : A ? F and there exists ? ? ? such that

F. Let, . M. ?x, and . @u, There exists A ? u such that A ? F ? ?x.M ? . So there exists ? ? ? such that ? ? ? ? ?? ?x.M : A ? F . Hence, there exists U such that

F. Conversely and . ?u, There exists ? ? (?, x ? u) such that ? ? ? ? ?? M : F . ? If x ? f v(M ), then there exist ? 1 ? ? and A ? u such that ? = ? 1 , x : A (using Lemma 5.1). So we have ? 1 ? ? ? ?? ?x

F. ?. Let, Hence there exist ? 1 , ? 2 , A and U such that ? = ? 1 ? ? 2

?. Hence-there-exist and U. Such-that-?-?-?-?, ? If U ? N ? there exist A and ? such that

F. Conversely and ?. Such, (x) = ?, so there exists A ? ?(x). Also, there exist ? ? and U such that ? = (? ?

F. Let, So there exists ? ? ? such that ? ? ? ? ?? C y,z x (M ) : F . Hence there exist ? ? , U , V 1 and V 2 such, V 1 ? V 2 )) and ? ? , x : U, y : V 1 , z : V 2 ? ? ? ?? M : F

?. Therefore and U. ?. , V 1 ? V 2 ) ? ?(x) or U ? (V 1 ? V 2 ) = ?. So U , V 1 and V 2 are either equal to ? or are in ?(x) Hence (? ? , x : U, y : V 1 , z : V 2 ) ? (?, y ? ?(x), z ? ?(x)), Therefore F ? M ?,y ??(x),z ??(x)

F. Conversely and . ??, z ??(x) , then there exists ? ? (?, x ? ?(x), y ? ?(y)). So there exist ? ?, 1 and V 2 such that ? = (? ? , x : U, y : V 1 , z : V 2 ) and U , V 1 and V 2 are