V. Mar, G. Aponte, and . Castagna, Programmation modulaire avec surcharge et liaison tardive, Journ ees Francophones des Langages Applicatifs, 1996.

H. Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science, 1991.

N. Bourbaki, El ements de Math ematiquee Th eorie des Ensembles, c hapter IV, 1970.

G. Castagna, Surcharge, sous-typage et liaison tardive : fondements fonctionnels de la programmation orient ee objets. T h ese de doctorat, Laboratoire d'Informatique de l'Ecole Normale Sup erieure, 1994.

]. C. Ccf-+-95, J. Cornes, J. Courant, G. Filli^-atre, P. Huet et al., The Coq Proof Assistant Reference Manual Version 5, INRIA, vol.10, 1995.

T. Coquand and G. Huet, The calculus of constructions, Inf. Comp, vol.76, pp.95-120, 1988.
URL : https://hal.archives-ouvertes.fr/inria-00076024

E. Contejean and C. March-e.-cime, Completion modulo e, 7th International Conference o n R ewriting Techniques and Applications, 1996.

T. Coquand, A meta-mathematical investigation of a Calculus of Constructions. Private Communication, 1987.

J. El and C. , A module calculus enjoying the subject-reduction property, LIP, 1996.

R. Di and C. , Isomorphisms of types: from -calculus to information retrieval and language design, Progress in Theoretical Computer Science, 1995.

W. M. Farmer, J. D. Guttman, and F. J. Thayer, The IMPS User's Manual. The MITRE Corporation, 1995.

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, Theoretical Computer Science. C a m bridge University Press, 1989.

R. Harper, F. Honsell, and G. Plotkin, A framework for deening logics, Preliminary version appeared in Proc. 2nd IEEE Symposium on Logic in Computer Science, vol.40, pp.194-204, 1987.

R. Harper and M. Lillibridge, A type-theoretic approach to higher-order modules with sharing, 21st Symposium on Principles of Programming Languages, pp.123-137, 1994.

R. Harper and F. Pfenning, A module system for a programming language based on the LF logical framework, 1992.

P. Mark and . Jones, Using parameterized signatures to express modular structures, 23rd S y m p osium on Principles of Programming Languages, 1996.

]. S. Kstar, D. Kahrs, A. Sannella, and . Tarlecki, The deenition of Extended ML: a gentle introduction, Theoretical Computer Science

X. Leroy, Manifest types, modules, and separate compilation, 21st symp. Principles of Progr. Lang., pages 109{122, 1994.
URL : https://hal.archives-ouvertes.fr/hal-01499976

X. Leroy, Applicative functors and fully transparent higher-order modules, 22nd Symposium on Principles of Programming Languages, pp.142-153, 1995.
URL : https://hal.archives-ouvertes.fr/hal-01499966

Z. Luo, Ecc: an extended calculus of constructions, Proc. of IEEE 4th Ann. Symp. on Logic In Computer Science, 1989.

D. B. Macqueen, 35 pages. An earlier version appeared in, Proc. 1984 ACM Conf. on Lisp and Functional Programming, vol.2, 1985.

L. Magnusson and B. Nordstrr, The ALF proof editor and its proof engine, Types for Proofs and Programs, vol.806, pp.213-237, 1994.

C. Paulin-mohring, Inductive deenitions in the system Coq : Rules and Properties, 1993.

R. Pollack, The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions, 1994.

R. Frann-cois, Typage de la surcharge dans un langage fonctionnel. T h ese, Alcool, vol.90, 1990.

R. Frann-cois, The Alcool 90 report

A. Saibi, , 1996.

D. Sannella, Formal program development in Extended ML for the working programmer, Proc. 3rd BCS/FACS Workshop on Reenement, pp.99-130, 1990.

P. S-e-v-eri and E. Poll, Pure type systems with deenitions, Lecture Notes in Computer Science, vol.813, 1994.

M. Takahashi, Parallel reductions in -calculus, 1993.