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

L. Cardelli, Typeful programming, Formal description of programming concepts, pp.431-507, 1989.

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

L. Cardelli and X. Leroy, Abstract types and the dot notation, Proceedings IFIP TC2 working conference o n p r ogramming concepts and methods, 1990.
URL : https://hal.archives-ouvertes.fr/hal-01499980

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

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.

;. P. H-+-92 and . Hudak, Report on the Programming Language Haskell: A no-strict purely Functional Language, ACM Sigplan Notices, vol.27, issue.5, 1992.

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, R. Milner, and M. Tofte, A type discipline for program modules, TAPSOFT 87, vol.250, pp.308-319, 1987.

R. Harper, R. Milner, and M. Tofte, The deenition of Standard M L, 1990.

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

.. P. Mark and . Jones, An Introduction to Gofer, 1991.

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

X. Leroy, , 1996.

J. C. Mitchell and G. D. Plotkin, Abstract types have existential type, ACM Trans. Prog. Lang. Syst, vol.10, issue.3, pp.470-502, 1988.

C. Benjamin and . Pierce, Bounded quantiication is undecidable, 19th Symposium on Principles of Programming Languages, pp.305-315, 1992.

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

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

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

N. Wirth, Programming in Modula-2. T exts and Monographs in Computer Science, 1983.