?. If, ? then there exists ? ? t : ? such that t is in ? -normal form

. Proof, As in the proof of Thm. 2, but using Lem. 7 (?) for soundness, Thm. 4.1 and Lem. 7 (?) for completeness

R. 1. Barendregt, The Lambda Calculus: Its Syntax and Semantics, 1984.

C. Ben-yelles, Type-assignment in the lambda-calculus; syntax and semantics, 1979.

A. Bernadet and S. Lengrand, Non-idempotent intersection types and strong normalisation, Logical Methods in Computer Science, vol.9, issue.4, p.2013
DOI : 10.2168/LMCS-9(4:3)2013
URL : https://hal.archives-ouvertes.fr/hal-00906778

M. W. Bunder, The inhabitation problem for intersection types, CATS'08, CRPIT 77, pp.7-14, 2008.

D. D. Carvalho, S` emantique de la logique linéaire et temps de calcul, 2007.

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

E. , D. Benedetti, and S. Rocca, Bounding normalization time through intersection types, ITRS'12, pp.48-57, 2013.

P. , D. Gianantonio, F. Honsell, and M. Lenisa, A type assignment system for game semantics, Theoretical Computer Science, vol.398, pp.150-169, 2008.

T. Ehrhard, The Scott model of linear logic is the extensional collapse of its relational model, Theoretical Computer Science, vol.424, pp.20-45, 2012.
DOI : 10.1016/j.tcs.2011.11.027
URL : https://hal.archives-ouvertes.fr/hal-00369831

J. R. Hindley, Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, 2008.

C. B. Jay and D. Kesner, First-class patterns, Journal of Functional Programming, vol.9, issue.02, pp.191-225, 2009.
DOI : 10.1016/j.tcs.2008.01.019
URL : https://hal.archives-ouvertes.fr/hal-00524750

D. Kesner and D. Ventura, Quantitative Types for the Linear Substitution Calculus, TCS, 2014.
DOI : 10.1007/978-3-662-44602-7_23
URL : https://hal.archives-ouvertes.fr/hal-01402078

A. J. Kfoury, A linearization of the Lambda-calculus and consequences, Journal of Logic and Computation, vol.10, issue.3, pp.411-436, 2000.
DOI : 10.1093/logcom/10.3.411

A. J. Kfoury and J. B. Wells, Principality and type inference for intersection types using expansion variables, Theoretical Computer Science, vol.311, issue.1-3, pp.1-70, 2004.
DOI : 10.1016/j.tcs.2003.10.032
URL : http://doi.org/10.1016/j.tcs.2003.10.032

J. L. Krivine, Lambda-Calculus, Types and Models, 1993.
URL : https://hal.archives-ouvertes.fr/cel-00574575

T. Kurata and M. Takahashi, Decidable properties of intersection type systems, TLCA'95, pp.297-311, 1995.
DOI : 10.1007/BFb0014060

H. Mairson and P. M. Neergaard, Types, potency, and idempotency: why nonlinearity and amnesia make a type system work, ICFP'04, pp.138-149, 2004.

M. Pagani and S. Rocca, Linearity, non-determinism and solvability, Fundamenta Informaticae, vol.103, pp.358-373, 2010.

M. Pagani and S. Rocca, Solvability in Resource Lambda-Calculus, FOSSACS'10, pp.358-373, 2010.
DOI : 10.1007/978-3-642-12032-9_25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.610.213

L. Paolini, M. Piccolo, and S. Rocca, Logical relational lambdamodels

P. Urzyczyn, Abstract, The Journal of Symbolic Logic, vol.7, issue.03, pp.1195-1215, 1999.
DOI : 10.1016/0304-3975(79)90006-9

S. Van-bakel, Complete restrictions of the intersection type discipline, Theoretical Computer Science, vol.102, issue.1, pp.135-163, 1992.
DOI : 10.1016/0304-3975(92)90297-S