*********************************************************************
*                    LIENS Ecole Normale Superieure                 *
*                                                                   *
*                           Groupe de travail                       *
*               'Semantique et Interpretation Abstraite'            *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 10h--12h                         *
*                    Salle Henri Cartan B, etage -2                 *
*                   DMI ENS 45 rue d'Ulm 75005 Paris                *
*********************************************************************

*** Vendredi 4 juin 1993 ******* Relache ****************************

*** Vendredi 11 juin 1993 ****** Seminaire ******* Henri Cartan B ***

Elimination de variables dans les systemes de contraintes lineaires 
generalisees.

Jean-Louis IMBERT (GIA, Marseille)

Resume: 	L'importance de l'elimination de variables dans les langages 
de type CLP, vient d'une part de la production de variables auxiliaires 
introduites lors de l'execution d'un programme, d'autre part de leur 
multiplication en cours de traitement. Cette elimination est presque 
toujours souhaitable pour presenter un resultat final. Elle peut aussi 
accroitre l'efficacite dans les  etapes intermediaires.

Nous nous placons dans le cadre restreint des systemes generalises de 
contraintes lineaires. Un systeme generalise de contraintes lineaires 
est compose d'un sous-systeme d'equations E, d'un sous-systeme 
d'inequations I (<=), et d'un sous-systeme de disequations D (\not =).
Un grand nombre de travaux ont ete realises sur l'elimination de 
variables de systemes lineaires d'equations et d'inequations (<=) 
[Fourier, Dines, Cernikov, Kohler, Duffin, Lassez, Imbert...].
Le cas des disequations (\not) a ete tres peu aborde, et seulement 
dans des cas trop generaux ou trop restraints.
	
Nous etablissons tout d'abord que l'operation d'elimination de variables 
sur un systeme generalise de contraintes lineaires E,I,D, a pour resultat 
un systeme generalise de contraintes lineaires E',I',D'. Nous montrons 
ensuite que E',I' ne depend pas de D, et que les disequations de D sont 
independantes les unes des autres pour l'operation d'elimination.
Nous presentons alors deux algorithmes d'elimination de variables sur le 
sous-systeme D. Le premier algorithme peut s'integrer facilement dans un 
algorithme traitant l'elimination sur les inequations par la methode de 
Fourier. Les variables sont eliminees l'une apres l'autre.
	Le second algorithme suppose connue la projection E',I', et repose 
sur de nouvelles proprietes que nous etablissons. Il elimine globalement 
les variables en une seule operation. Les nombreuses independances mises a 
jour permettent un haut degre de parallelisme que nous exploitons. 
	Enfin, ce second algorithme fournit des contraintes sous une forme 
canonique definie par J.L. Lassez et K. MacAloon.

*** Vendredi 18 juin 1993 ****** Seminaire ******* Henri Cartan B ***

Interpretation abstraite de langages a parallelisme de donnees (data
parallel).

Alain DEUTSCH (INRIA, Rocquencourt)

Resume: non parvenu.

*** Vendredi 25 juin 1993 ****** Seminaire ******* Henri Cartan B ***

Interpretation Abtraite et typages, un exemple d'application :
l'analyse de necessite

Bruno MONSUEZ (LIENS, Paris)

Resume: L'analyse de necessite fut l'une des premieres analyses a 
etre definie en utilisant le formalisme de l'interpretation abstraite. 
Toutefois, certains recents developpements ont exhibe de nouvelles 
versions d'analyse de necessite basees sur des regles d'inferences.
Nombreux sont ceux qui pretendent que l'approche basee sur les regles
d'inferences est plus efficace. Cependant il n'en est rien. En effet,
en utilisant l'approche developpee pour caracteriser les systemes
de types classiques comme ceux de ML,ML+,Miranda,Coppo-Dezani comme
une interpretation abstraite, nous montrons qu'il est possible 
d'obtenir les systemes de regles d'inferences comme ceux de Kuo & 
Mishra. De plus, nous heritons de toute la panoplie des instruments 
que possedent l'interpretation abstraite, et plus particulierement 
des operateurs d'elargissement. De ce fait, il est possible d'obtenir 
des resultats plus precis que ceux traditionnellement obtenu par les 
systemes de regles d'inference, principalement dans le cas des 
expressions recursives, et ce pour un cout tout a fait negligeable.

*********************************************************************