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

[. Boudol, The lambda-calculus with multiplicities, 1993.
DOI : 10.1007/3-540-57208-2_1
URL : https://hal.archives-ouvertes.fr/inria-00074646

M. Coppo and M. Dezani, A new type-asssignment for ¢ -terms. Archive für mathematische Logik und Grundlagenforschung, pp.139-156, 1978.

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-683, 1980.
DOI : 10.1305/ndjfl/1093883253

[. Coppo, M. Dezani-ciancaglini, and B. Venneri, Functional Characters of Solvable Terms, Zeitschrift für matematische Logik und Grundlagen der Mathematik, pp.44-58, 1981.
DOI : 10.1002/malq.19810270205

O. Gan80-]-robin and . Gandy, Proofs of strong normalisation

. Hinley, H. B. To, and . Gentzen, Curry: essays on combinatory logic, ¢ calculus and formalism Untersuchungen u ¨ber das logische Schließen I, Traduction Française de R. Feys et J. Ladrière: Recherches sur la déduction logique, pp.457-477176, 1934.

J. Girard, Proof-Theory and Logical Complexity ? vol. I. Studies in Proof Theory, Bibliopolis, 1987.

]. J. Hin82 and . Hindley, The simple semantics for Coppo-Dezani-Sallé types, 5 ¡ International Symposium on Programming (Torino), pp.212-226, 1982.

C. Retoré-[-hin84 and ]. J. Hindley, Coppo-Dezani types do not correspond to propositional logic, Theoretical Computer Science, vol.28, pp.235-236, 1984.

[. Ja´skowskija´skowski, On the rules of supposition in formal logic, Studia logica, vol.1, 1934.

J. Krivine, Lambda Calcul ? Types et Modèles, Etudes et Recherches en Informatique. Masson, 1990.

. Pottinger, A type assignment for the strongly normalizable ¢ terms, To H.B. Curry: Essays on Combinatory Logic " ¢ -calculus and formalism, pp.561-577, 1980.

D. Prawitz, Natural Deduction, a Proof-theoretical Study

D. Prawitz, Ideas and Results in Proof Theory, Proceedings of the second scandinavian logic symposium, Sudies in Logic, pp.235-307, 1971.
DOI : 10.1016/S0049-237X(08)70849-8

[. Sallé, Une extension de la theorie des types en ??-calcul, 5 ¡ International Colloquium on Automata , Languages and Programming, 1978.
DOI : 10.1007/3-540-08860-1_30

I. Unité-de-recherche, V. Lorraine, and I. Le-`-sle-`-le-`-s-nancy-unité-de-recherche, Technopôle de Nancy-Brabois, Campus scientifique, 615 rue du Jardin Botanique, pp.38031-38032

I. Unité-de-recherche and . Rocquencourt, Domaine de Voluceau, Rocquencourt, BP 105, 78153 LE CHESNAY Cedex Unité de recherche INRIA Sophia-Antipolis, 2004.