Abstract FR:

Un des problemes souleves par la formalisation de mathematiques dans un assistant de preuve est la lourdeur de toute preuve, et de toute formalisation. Une approche pour pallier cette difficulte seconde consiste a etablir des environnements de developpements de preuves plus flexibles et expressifs fondes sur des formalismes aussi puissants que possible. Ces formalismes sont souvent fondes sur les paradigmes de la programmation fonctionnelle. Or il existe dans ce domaine des systemes de modules qui facilitent la gestion de gros developpements, tel le systeme de modules de sml, qui s'integre bien dans une large classe de langages de programmation. En ce qui concerne la preuve mathematique, les notions de structures sont comparables a celles definies par bourbaki. La notion de foncteur correspond ainsi a la parametrisation d'une theorie, notion essentielle dans la formalisation mathematique car elle permet d'etablir des theories sur des structures abstraites qui sont comparables a des bibliotheques de programmes que l'on peut instancier sur toute instance concrete de la structure consideree. Cependant, les systemes de modules existants presentaient des defauts les rendant inutilisables dans la perspective d'un formalisme logique. J'en ai donc propose une variante corrigeant ces defauts. J'ai montre qu'elle s'adaptait a la classe des systemes de types purs. Les resultats sont beaucoup plus statisfaisants sur le plan theorique, car le formalisme logique obtenu n'est pas seulement une extension du systeme initial mais est aussi une extension de la correspondance de curry-howard entre programmation et raisonnement. J'ai reussi a montrer les resultats metatheoriques qu'on attend d'un tel systeme : auto-reduction, confluence, normalisation forte, conservativite logique de l'extension par modules, consistance logique de l'extension. En outre, cette etude apporte de nouveaux elements pour la comprehension des notions de classes et d'heritage des langages orientes objets.