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

H. P. Barendregt, Introduction to Generalised Type Systems, Journal of Functional Programming, vol.1, issue.2, pp.125-154, 1991.

H. P. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, pp.118-310, 1992.
DOI : 10.1017/cbo9781139032636

S. Berardi, Towards a Mathematical Analysis of Type Dependence in Coquand?Huet Calculus of Constructions and the Other Systems in Barendregt's Cube, 1988.

T. Coquand, Metamathematical Investigations of a Calculus of Constructions Academic press, Logic and Computer Science, pp.91-122, 1991.

T. Coquand and G. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988.
DOI : 10.1016/0890-5401(88)90005-3

URL : https://hal.archives-ouvertes.fr/inria-00076024

H. B. Curry, Functionality in Combinatory Logic, Proc. Nat. Acad. Sci. U.S.A, pp.584-590, 1934.
DOI : 10.1073/pnas.20.11.584

G. Dowek, The undecidability of typability in the Lambda-Pi-calculus
DOI : 10.1007/BFb0037103

H. Geuvers and M. Nederhof, Modular Proof of Strong Normalization for the Calculus of Constructions, Journal of Functional Programming, vol.1, issue.2, pp.155-189, 1991.

P. Giannini, F. Honsell, and S. Ronchi-della-rocca, Type inference: some results, some problems, Fundamenta Informaticae, vol.19, issue.12, pp.87-126, 1993.

P. Giannini and S. Ronchi-della-rocca, Characterization of typings in polymorphic type discipline, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.61-70, 1988.
DOI : 10.1109/LICS.1988.5101

J. Y. Girard, The system F of variable types, fifteen years later, Theoretical Computer Science, vol.45, pp.159-192, 1986.
DOI : 10.1016/0304-3975(86)90044-7

J. W. Klop, Combinatory Reduction Systems, 1980.

D. Leivant, Polymorphic type inference, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '83, pp.88-98, 1983.
DOI : 10.1145/567067.567077

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4

J. C. Reynolds, Towards a theory of type structure, Proceedings of Programming Symposium, pp.408-425, 1974.
DOI : 10.1007/3-540-06859-7_148

S. Van-bakel, L. Liquori, S. Ronchi-della-rocca, and P. Urzyczyn, Comparing cubes, Proceedings of LFCS '94. Third International Symposium on Logical Foundations of Computer Science, pp.353-365, 1994.
DOI : 10.1007/3-540-58140-5_33

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