Abstract FR:

Les opérations classiques de transformations de programmes logiques (pliage, dépliage,. . . ) préservent la sémantique des programmes au sens du plus petit modèle de Herbrand et au sens de l'ensemble des substitutions-réponses. Ces transformations ne peuvent pas être appliquées directement à des programmes écrits en Prolog complet (avec des effets de bord) car elles ne préservent pas l'équivalence opérationnelle des programmes. Nous avons donc défini une équivalence opérationnelle associée au comportement observable des programmes. Cette équivalence nous permet de traiter les programmes réels. Nous avons ensuite étudié les transformations préservant une telle équivalence. Puis notre travail s'est divisé en deux parties: l'optimisation de programmes Prolog complet, en les manipulant par nos transformations et en utilisant des informations sur les programmes provenant d'un analyseur statique; l'utilisation des transformations de programmes comme outils de preuve pour la validation de méta-interpréteurs et l'obtention de résultats d'indécidabilité pour des classes de petits programmes.