Abstract FR:

Le typage polymorphique generique de certains systemes de programmation logique presente plusieurs problemes que nous exposons a la lumiere de l'un de ces systemes: prolog. Nous proposons une discipline de typage polymorphique parametrique qui resout ces problemes. Nous la presentons comme une extension de prolog que nous appelons #2prolog. Prolog est un langage recent de programmation en logique qui permet de decrire des problemes logiciels (modularite, portee, duree de vie) par des moyens purement logiques. Le formalisme de prolog est issu de la combinaison du -calcul et de la logique intuitionniste restreinte aux formules hereditaires de harrop. Ce langage peut etre defini comme une double extension de prolog avec des termes d'ordre superieur et de nouveaux constructeurs logiques. Comme tout langage de programmation logique, un systeme de deduction avec unification definit sa semantique operationnelle. Prolog doit etre type pour que l'unification des -termes soit bien definie. Le typage adopte dans les mises en uvre courantes de prolog est un typage simple avec des variables de type, c'est-a-dire avec du polymorphisme generique, comme dans ml. Un tel typage polymorphe a aussi ete etudie pour prolog mais a rarement ete implemente. L'experience de la programmation revele les limites de ce polymorphisme pour les langages de programmation logique. Nous montrons que le polymorphisme parametrique de la theorie du -calcul polymorphe, #2, convient mieux aux langages de programmation logique. Quelques problemes sont resolus simultanement. Tout d'abord, la condition de tete qui est importante mais restrictive pour les predicats avec du polymorphisme generique est trivialement respectee avec du polymorphisme parametrique. Ensuite, le typage polymorphique generique ne donne pas de statut formel aux types devant etre representes a l'execution. Dans un systeme avec du polymorphisme parametrique, ces types peuvent etre passes en parametre des termes et ainsi avoir un statut formel. Enfin, avec du polymorphisme generique, un predicat polymorphe passe en parametre ou defini modulairement ne peut etre utilise de facon non generique, c'est-a-dire dans differents contextes. Dans un systeme avec du polymorphisme parametrique, les variables de type peuvent etre quantifiees localement, ce qui permet de preciser le polymorphisme des parametres et des definitions modulaires. Le formalisme de #2prolog est issu de la combinaison de #2 et de la logique intuitionniste restreinte aux formules hereditaires de harrop. #2prolog est une extension de prolog par des quantifications de type au niveau des types, des termes et des formules ainsi que par une construction pour exprimer une garde de type. Nous formalisons la discipline de type de #2prolog par un systeme de deduction de type. Nous definissons et formalisons la semantique de #2prolog, et une operation de completion de type qui permet a un utilisateur d'omettre la plupart des annotations de type. Tout ceci peut etre facilement applique a un langage tel que prolog par simple restriction aux formules de horn