********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h--16h * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 3 fe'vrier 1995 **************************************** Relache. *** Vendredi 10 fe'vrier 1995 *************************************** Caracte'risation du syste` me F par interpre'tation abstraite Bruno MONSUEZ (LIENS) Re'sume' : Dans de precedentes publications, nous avons expose comment les systemes d'inference de types d'Hyndley/Milner ou de Coppo pouvaient etre reformules en utilisant le formalisme de l'interpretation abstraite. Nous nous proposons de generaliser cette approche au systeme F. Dans cet expose, nous exhiberons tout d'abord une abstraction permettant d'abstraire l'ensemble des valeurs que le programme peut-etre amene a manipuler par un type du systeme F. Dans un deuxieme temps, nous montrerons comment il est possible a l'aide de l'abstraction precedemment definie de deriver les regles d'assignement de types du systeme F a partir de la semantique dynamique du langage a l'aide de l'abstraction precedemment definie. *** Vendredi 17 fe'vrier 1995 *************************************** Mecanismes eval/quote et logique modale S4 Jean GOUBAULT (BULL) Re'sume' : L'isomorphisme de Curry-Howard e'tablit un lien entre un langage de programmation (le lambda-calcul) et logique (la logique intuitionniste). Ces dernie`res anne'es, plusieurs chercheurs se sont aperc,us que ce lien entre langages et logique n'e'tait pas isole', et on a pu voir des interpretations fonctionnelles de divers fragments de la logique lineaire, ainsi que de la logique classique, notamment. Par curiosite, je me suis interesse a la logique modale S4, due a Clarence Lewis, et je montrerai comment on arrive naturellement a une interpretation fonctionnelle utilisant des operations eval et quote dans le style propose par le langage Lisp. En guise d'applications, je mentionnerai notamment ce qu'eval/quote peut apporter a un langage de style ML et comment. Honnetement, je prendrai surtout un malin plaisir a utiliser des arguments logiques de toute beaute (l'interpretation fonctionnelle) pour justifier une construction de programmation reputee sale (eval/quote). *** Vendredi 24 fe'vrier 1995 *************************************** Analyse se'mantique de Concurrent Pascal et Model-Checking abstrait Re'gis CRIDLIG (LIENS) Re'sume' : Nous allons pre'senter une se'mantique vraiment paralle`le d'un sous-ensemble de Pascal muni de la construction paralle`le Cobegin/ Coend et s'exe'cutant en me'moire partage'e. Cette se'mantique, base'e sur un syste`me de transitions de dimension supe'rieure, est capable de mode'liser le caracte`re asynchrone de l'exe'cution des processus paralle`les, me^me lorsqu'ils interfe`rent. Par interpre'tation abstraite utilisant un repliage des e'tats avec un ope'rateur d'e'largissement, nous montrons comment obtenir un automate de taille finie qui puisse servir a` l'analyse statique du programme CPASCAL conside're'. Les proprie'te's abstraites auxquelles on s'inte'resse peuvent alors e^tre calcule'es par model-checking sur l'automate abstrait obtenu pre'ce'demment : pour traiter la ne'gation, l'interpre'tation abstraite doit combiner a` la fois une approximation supe'rieure et une approximation infe'rieure. *********************************************************************