Programmation modulaire avec surcharge et liaison tardive, Journ ees Francophones des Langages Applicatifs, 1996. ,
Lambda calculi with types, Handbook of Logic in Computer Science, 1991. ,
El ements de Math ematiquee Th eorie des Ensembles, c hapter IV, 1970. ,
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. ,
The Coq Proof Assistant Reference Manual Version 5, INRIA, vol.10, 1995. ,
The calculus of constructions, Inf. Comp, vol.76, pp.95-120, 1988. ,
URL : https://hal.archives-ouvertes.fr/inria-00076024
Completion modulo e, 7th International Conference o n R ewriting Techniques and Applications, 1996. ,
A meta-mathematical investigation of a Calculus of Constructions. Private Communication, 1987. ,
A module calculus enjoying the subject-reduction property, LIP, 1996. ,
Isomorphisms of types: from -calculus to information retrieval and language design, Progress in Theoretical Computer Science, 1995. ,
The IMPS User's Manual. The MITRE Corporation, 1995. ,
Proofs and Types, Theoretical Computer Science. C a m bridge University Press, 1989. ,
A framework for deening logics, Preliminary version appeared in Proc. 2nd IEEE Symposium on Logic in Computer Science, vol.40, pp.194-204, 1987. ,
A type-theoretic approach to higher-order modules with sharing, 21st Symposium on Principles of Programming Languages, pp.123-137, 1994. ,
A module system for a programming language based on the LF logical framework, 1992. ,
Using parameterized signatures to express modular structures, 23rd S y m p osium on Principles of Programming Languages, 1996. ,
The deenition of Extended ML: a gentle introduction, Theoretical Computer Science ,
Manifest types, modules, and separate compilation, 21st symp. Principles of Progr. Lang., pages 109{122, 1994. ,
URL : https://hal.archives-ouvertes.fr/hal-01499976
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
Ecc: an extended calculus of constructions, Proc. of IEEE 4th Ann. Symp. on Logic In Computer Science, 1989. ,
35 pages. An earlier version appeared in, Proc. 1984 ACM Conf. on Lisp and Functional Programming, vol.2, 1985. ,
The ALF proof editor and its proof engine, Types for Proofs and Programs, vol.806, pp.213-237, 1994. ,
, Inductive deenitions in the system Coq : Rules and Properties, 1993.
The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions, 1994. ,
Typage de la surcharge dans un langage fonctionnel. T h ese, Alcool, vol.90, 1990. ,
The Alcool 90 report ,
, , 1996.
Formal program development in Extended ML for the working programmer, Proc. 3rd BCS/FACS Workshop on Reenement, pp.99-130, 1990. ,
Pure type systems with deenitions, Lecture Notes in Computer Science, vol.813, 1994. ,
Parallel reductions in -calculus, 1993. ,