?. If, then there exist ? and U such that

. Proof, By the fact that ? ? ? is defined point-wise

M. Assume and =. ?. Then, Therefore, there exists ? ? ? such that ? M : A. By Theorem 2, M is strongly normalising. 3. ? Assume F ? x ? . Then, there exists ? ? ? such that ? x, We also have ?(x) ? ?(x). Hence, F ? ?(x)

@. Assume and F. , Then, (x : F ) ? ? and x : F x : F . Therefore, F ? x ?

@. Assume and F. ?. Then, Therefore, there exist ? 1 , ? 2 and A such that ? = ? 1 ? ? 2 , ? 1 M : A ? F and ? 2 N : A

]. S. Bibliography-[-abr93 and . Abramsky, Computational interpretations of linear logic, Theoret. Comput. Sci, vol.111, pp.3-57, 1993.

]. N. Bbdh93, G. Benton, V. Bierman, M. De-paiva, and . Hyland, A term calculus for intuitionistic linear logic, Proc. of the 1st Int. Conf. on Typed Lambda Calculus and Applications, pp.75-90, 1993.

H. Barendregt, M. Coppo, M. Dezani-ciancaglini, A. Bucciarelli, T. Ehrhard et al., A filter lambda model and the completeness of type assignment, Ber09] A. Bernadet. Fixpoints and strong normalisation. Internship report, pp.931-940, 1983.
DOI : 10.1002/malq.19800261902

]. A. Bl11a, S. Bernadet, and . Lengrand, Complexity of strongly normalising ?-terms via non-idempotent intersection types, Proc. of the 14th Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS'11), pp.46-47, 2011.

]. A. Bl11b, S. Bernadet, ]. Lengrandbl13, S. Bernadet, . Lengrandbm03-]-p et al., Filter models: non-idempotent intersection types, orthogonality and polymorphism Non-idempotent intersection types and strong normalisation Soft lambda-calculus: a language for polynomial time computation. CoRR, cs Alcune proprietà delle forme ?-?-normali nel ?K-calcolo, Proc. of the 20th Annual Conf. of the European Association for Computer Science Logic (CSL'11), LIPIcs. Schloss Dagstuhl LCI Dezani-Ciancaglini. A new type assignment for lambda-terms. Archiv für mathematische Logik und Grundlagenforschung, pp.61-68, 1968.

A. Heyting, Intuitionism: an introduction. Studies in logic and the foundations of mathematics, 1971.

]. W. How80 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.

F. [. Kesner and . Renaud, A prismoid framework for languages with resources, Theoretical Computer Science, vol.412, issue.37, pp.4867-4892, 2011.
DOI : 10.1016/j.tcs.2011.01.026

URL : https://hal.archives-ouvertes.fr/hal-00625598

]. J. Kvovr93, V. Klop, F. Van-oostrom, ]. A. Van-raamsdonkkw99, J. B. Kfoury et al., Combinatory reduction systems: introduction and survey Principality and decidable type inference for finite-rank intersection types, Proc. of the 26th Annual ACM Symp. on Principles of Programming Languages (POPL'99) Lafont. Soft linear logic and polynomial timeLei86] D. Leivant. Typing and computational properties of lambda expressions Lawvere and S. H. Schanuel. Conceptual Mathematics: A First Introduction to Categories, pp.279-308, 1986.

H. [. Neergaard, . M. Mairsonpit03-]-a, and . Pitts, Types, potency, and idempotency: why nonlinearity and amnesia make a type system work Nominal logic, a first order theory of names and binding, Proc. of the 9th ACM Intern. Conf. on Functional Programming, pp.138-149, 2003.

]. F. Ren11 and . Renaud, Les ressources explicites vues par la théorie de la réécriture, p.36, 2011.

]. S. Sal10, . S. Salvatisco82a-]-d, and . Scott, On the Membership Problem for Non-Linear Abstract Categorial Grammars Domains for denotational semantics, J. of Logic, Language, and Information Lecture Notes in Computer Science, vol.19, issue.140 8, pp.163-183, 1982.

]. D. Sco82b and . Scott, Domains for denotational semantics, Proc. of the 9th Intern, pp.577-613, 1982.

W. W. Taittur36-]-a, ]. S. Turing, and . Van-bakel, A realizability interpretation of the theory of species On computable numbers, with an application to the Entscheidungsproblem Intersection Type Assignment Systems, Logic ColloquiumvH02] J. van Heijenoort. From Frege to Gödel : A Source Book in Mathematical LogicSource Books in the History of the Sciences), pp.240-251, 1936.

]. F. Van-raamsdonk, P. Severi, M. H. Sørensen, H. B. Xiwel96-]-j, and . Wells, Perpetual Reductions in??-Calculus, Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS), pp.173-225, 1996.
DOI : 10.1006/inco.1998.2750

M. If and . Term, Var ? Term, we define bind(M, f ) the term defined by induction on M as follow: bind(x, f ) = f (x) bind(M N, f ) = bind(M, f )bind(N, f ) bind(?M, f ) = ?bind(M, f ) with f : Var ? Term the unique function such that, (x)) (?x ? Var

M. Assume, . Term, ?. Var, and . Var, Then f : Var ? Term and bind(M, f ) = map(M, f )

M. Assume and . Term, Then for all f, g : Var ? Term, if we have ?x ? fv(M ), f (x) = g(x) then bind(M, f ) = bind(M, g)

. Lemma-46, Assume M ? Term and f : Var ? Var, Then fv(map(M, f )) = {f (x) | x ? fv(M )}

M. Assume, . Term, ?. Var, and . Term, Then: fv(bind(M, f )) = x?fv(M ) fv(f (x))

. Lemma-47, Assume M ? Term, f : Var ? Var and g : Var ? Term. Then g ? f : Var ? Term and bind(map(M, f ), g) = bind(M, g ? f )

M. Assume and . Term, f : Var ? Term, and g : Var ? Term We write h : Var ? Term defined by: ?x ? Var, h(x) = bind(f (x), g) Then we have bind(bind, g) = bind(M, h)

M. Assume, ?. Term, N. Var, and . Term, We write M {x := N } for bind(M, f ) with f : Var ? Term defined as follow: f (x) = N f (y) =

M. Assume and N. , ? Term and x, y ? Var, Then: ? If x / ? fv(M ), then M {x := N } = M

?. Assume-x, M. Var, and . Term, We write ?x

@. If and ?. , N then M {x := y} = N and if x = y then y / ? fv(M )

M. Assume, For all x, y ? Var we define < x, y >: Var ? Var defined as follow

M. Assume and N. Term, Then M = N if and only if M = ? N

. Proof, One way is by induction on M ? T Var and the other way is by induction on M = ? N

X. Assume and Y. , f : Var ? Term, and M ? Term such that for all x ? fv(M ), [f (x)] ?1 = ? 2 (x) ? ?, Then [bind(M, f )] ?1 = [M ] ?2 ? ?

X. Assume, X. Env, ?. Var, M. , and N. Term, Then [M {x := N }] ? = [M ] ? with ? ? Env X defined as follow: ? (x) =