H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, 1991.
DOI : 10.1017/cbo9781139032636

B. Barras and B. Bernardo, The Implicit Calculus of Constructions as a Programming Language with Dependent Types, Lecture Notes in Computer Science, vol.4962, pp.365-379, 2008.
DOI : 10.1007/978-3-540-78499-9_26
URL : https://hal.archives-ouvertes.fr/inria-00429543

J. Girard, P. Taylor, and Y. Lafont, Proofs and types, 1989.

P. Letouzey, Programmation fonctionnelle certifiée ? L'extraction de programmes dans l'assistant Coq, 2004.

Z. Luo, ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1990.
DOI : 10.1109/LICS.1989.39193

C. Paulin-mohring, Définitions Inductives en Théorie des Types d'Ordre Supérieur. Habilitation à diriger les recherches, 1996.

M. Tatsuta, Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
DOI : 10.1007/978-3-540-73228-0_26

J. B. Wells, Typability and type checking in System F are equivalent and undecidable, Annals of Pure and Applied Logic, vol.98, issue.1-3, pp.1-3111, 1999.
DOI : 10.1016/S0168-0072(98)00047-5