H. P. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, 1991.

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

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

H. B. Curry, Modified Basic Functionality in Combinatory Logic, Dialectica, 1969.

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

T. Coquand and G. Huet, The Calculus of Constructions, Information and Computation, pp.95-120, 1988.

G. Dowek, The undecidability of typability in the Lambda-Pi-calculus, Proc. Typed Lambda Calculi and Applications, pp.139-145, 1993.
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, R. Della-rocca, and S. , 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

P. Giannini, F. Honsell, R. Della-rocca, and S. , Type Inference: Some Results, Some Problems, Fundamenta Informaticae, vol.19, issue.12, pp.87-126, 1993.

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

B. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, 1993.
DOI : 10.1145/138027.138060

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

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