these

oN d’ordre: 000`THESE DE DOCTORAT DE´L’UNIVERSITE PARIS 6Sp´ecialit´eInformatiquepr´esent´ee parEmmanuel Coquerypour obtenir le grade de´Docteur de l’universite de Paris 6´Ecole doctorale : Informatique, T´el´ecommunications et Electronique de ParisUFR D’INFORMATIQUELaboratoire : INRIA-Rocquencourt´Equipe d’accueil : ContraintesTitre de la th`ese :Typage et programmation en logique avec contraintesSoutenue le 3 D´ecembre 2004 devant le jury compos´e de :Me. : Ir`ene Guessarian Pr´esidenteMM. : Jean Goubault-Larrecq RapporteursJan MaluszynskiFranc¸ois PottierMe. : V´eronique Donzeau-Gouge ExaminatriceM. : Franc¸ois Fages DirecteurR´esum´eLes langages logiques avec contraintes sont des langages non typ´es. Les pro-grammeurs qui utilisent ces langages b´en´eficient donc d’une grande souplesse deprogrammation, au d´etriment des avantages apport´es par le typage, en particulierla d´etection d’erreurs de programmation.Cette th`ese d´ecrit un syst`eme de types pour les langages logiques avec con-traintes, de sa formalisation `a sa mise en œuvre. Ce syst`eme combine poly-morphisme param´etrique, sous-typage et surcharge pour obtenir la souplessen´ecessaire au typage de programmes utilisant des techniques de programmationlogique avec contraintes comme la m´eta-programmation et l’utilisation conjointede diff´erents domaines de contraintes. Le syst`eme est prouv´e coh´erent par rap-port `a la r´esolution CSLD et par rapport `a un mod`ele d’ex´ecution ...