Soutenance de th
Forum 'Annonces' - Sujet créé le 2004-11-17
Bonjour,
J'ai le plaisir de vous annoncer ma soutenance de thèse intitulée
"Typage et programmation en logique avec contraintes"
et de vous inviter au pot qui suivra:
le vendredi 3 décembre 2004, à 14h30
à l'université Paris 6, Jussieu
tour 24, couloir 24-25, salle 301
Pour plus de précisions, voir:
http://contraintes.inria.fr/~coquery/these.fr.html
Résumé:
Les langages logiques avec contraintes sont des langages non typés. Les
programmeurs qui utilisent ces langages bénéficient donc d'une grande
souplesse de programmation, au détriment des avantages apportés par le
typage, en particulier la détection d'erreurs de programmation.
Cette thèse décrit un système de types pour les langages langages
logiques avec contraintes, de sa formalisation à sa mise en oeuvre. Ce
système combine polymorphisme paramétrique, sous-typage et surcharge
pour obtenir la souplesse nécessaire au typage de programmes utilisant
des techniques de programmation logique avec contraintes comme la
méta-programmation et l'utilisation conjointe de différents domaines de
contraintes. Le système est prouvé cohérent par rapport à la résolution
CSLD et par rapport à un modèle d'exécution typé avec substitutions. Un
algorithme de vérification des types avec inférence du type des
variables et gestion efficace de la surcharge a également été développé,
ainsi qu'un algorithme heuristique d'inférence de type pour les
prédicats.
Cette thèse s'intéresse également au problème de la satisfiabilité des
contraintes d'ordre dans les quasi-treillis, qui constituent des
structures de types riches, ajoutant ainsi de la souplesse au système de
type. Le problème de satisfiabilité est montré NP-complet dans le cas de
quasi-treillis dont les extrema sont des constantes en nombre fini. La
complexité de l'algorithme devient O(n3) dans le cas où toutes les
variables du système de contraintes sont bornées. Un algorithme pour le
calcul explicite de solutions est également présenté. De plus, cet
algorithme permet de tester la satisfiabilité dans des quasi-treillis
dont seuls les maxima sont des constantes en nombre fini. Ces résultats
sur les quasi-treillis sont généraux et leur portée n'est pas limitée au
typage.
Emmanuel Coquery
J'ai le plaisir de vous annoncer ma soutenance de thèse intitulée
"Typage et programmation en logique avec contraintes"
et de vous inviter au pot qui suivra:
le vendredi 3 décembre 2004, à 14h30
à l'université Paris 6, Jussieu
tour 24, couloir 24-25, salle 301
Pour plus de précisions, voir:
http://contraintes.inria.fr/~coquery/these.fr.html
Résumé:
Les langages logiques avec contraintes sont des langages non typés. Les
programmeurs qui utilisent ces langages bénéficient donc d'une grande
souplesse de programmation, au détriment des avantages apportés par le
typage, en particulier la détection d'erreurs de programmation.
Cette thèse décrit un système de types pour les langages langages
logiques avec contraintes, de sa formalisation à sa mise en oeuvre. Ce
système combine polymorphisme paramétrique, sous-typage et surcharge
pour obtenir la souplesse nécessaire au typage de programmes utilisant
des techniques de programmation logique avec contraintes comme la
méta-programmation et l'utilisation conjointe de différents domaines de
contraintes. Le système est prouvé cohérent par rapport à la résolution
CSLD et par rapport à un modèle d'exécution typé avec substitutions. Un
algorithme de vérification des types avec inférence du type des
variables et gestion efficace de la surcharge a également été développé,
ainsi qu'un algorithme heuristique d'inférence de type pour les
prédicats.
Cette thèse s'intéresse également au problème de la satisfiabilité des
contraintes d'ordre dans les quasi-treillis, qui constituent des
structures de types riches, ajoutant ainsi de la souplesse au système de
type. Le problème de satisfiabilité est montré NP-complet dans le cas de
quasi-treillis dont les extrema sont des constantes en nombre fini. La
complexité de l'algorithme devient O(n3) dans le cas où toutes les
variables du système de contraintes sont bornées. Un algorithme pour le
calcul explicite de solutions est également présenté. De plus, cet
algorithme permet de tester la satisfiabilité dans des quasi-treillis
dont seuls les maxima sont des constantes en nombre fini. Ces résultats
sur les quasi-treillis sont généraux et leur portée n'est pas limitée au
typage.
Emmanuel Coquery