*******************************************************************
*                   LIENS Ecole Normale Superieure                *
*                      Les vendredis de l'equipe                  *
*              'Semantique et Interpretation Abstraite'           *
*                              P. Cousot                          *
*             Salle J-L Verdier, Passage Vert, 14h--16h           *
*                 DMI ENS 45 rue d'Ulm 75005 Paris                *
*******************************************************************

*** Vendredi 6 novembre 1992 *** Reunion de travail ***************

Eric Goubault Des modeles du parallelisme.

*** Vendredi 12 novembre 1992, DEC PRL, 16h *** Soutenance de these 

Semantiques des langages imperatifs d'ordre superieur
et interpretation abstraite

Francois Bourdoncle (DEC-PRL)

Resume: L'interpretation abstraite ou analyse semantique d'un 
langage de programmation est une methode formelle permettant 
d'obtenir, de maniere statique (i.e. la compilation) et automatique, 
une description approchee du comportement dynamique (i.e. a 
l'execution) des programmes. Cette methode a ete appliquee, 
jusqu'ici, a des langages relativement simples (langages imperatifs, 
fonctionnels, logiques ou paralleles du premier ordre).  Or les 
langages de programmation modernes comme le langage Modula-3 ou 
meme des langages plus anciens comme Pascal comportent des 
mecanismes de programmation puissants (passage des parametres 
formels par reference, passage en parametre des procedures
locales, sauts a des labels non locaux, exceptions) qui augmentent
de maniere considerable leur puissance d'expression et leur
complexite semantique. Cette these aborde le probleme de 
l'interpretation abstraite des langages imperatifs d'ordre 
superieur. Dans une premiere partie, nous montrons que des 
interpretations abstraites trop ``naives'' de tels langages d'ordre 
superieur peuvent devenir a la fois extremement couteuses 
et imprecises. Pour remedier a ces problemes, nous introduisons 
une nouvelle semantique des langages imperatifs d'ordre superieur 
dont l'interpretation abstraite est precise et peu couteuse et
nous etablissons la correction de cette semantique pour une
classe non decidable de programmes comprenant en particulier la
classe decidable des programmes Pascal. Puis, dans la
seconde partie, nous abordons la technique du debugging abstrait
permettant d'effectuer une mise au point formelle des programmes et
nous presentons le systeme Syntox permettant d'effectuer
le debugging abstrait du langage Pascal par la determination
de l'intervalle de variation des variables scalaires des programmes.

DEC PRL 85, avenue Victor Hugo, 92563 Rueil-Malmaison

*** Vendredi 20 novembre 1992 *** Seminaire **********************

Parallelisme, automates et topologie algebrique

Eric Goubault (LIENS)

Resume : L'objet de ce seminaire est de presenter une generalisation 
des automates sequentiels classiques aux automates ``de dimension 
superieure'' qui fournissent un modele du ``vrai parallelisme'',
c'est a dire qu'ils distinguent choix non-deterministe et execution
concurrente. On montrera que la geometrie de ces automates nous 
permet de discuter de notions telles que: branchements, deadlocks, 
divergences, sequentiabilisation, mais aussi d'analyser un certain 
nombre d'equivalences semantiques comme la bisimulation, failure 
equivalence... Cette geometrie peut etre decrite purement 
algebriquement en utilisant des outils nous venant de la topologie 
algebrique. Le modele lui-meme a une expression algebrique 
directement en termes d'objets d'algebre homologique. Cela nous 
donne des methodes de calculs effectifs pour enumerer les deadlocks, 
semi-decider d'equivalences semantiques... Des exemples seront 
donnes en decrivant CCS dans notre formalisme.


*** Vendredi 27 novembre 1992 *** Reunion d'equipe ***************

Quelques idees naives sur les semantiques en style de passage a
la continuation.

Jean Goubault  (BULL)

Resume: le style de passage a la continuation (CPS) a permis dans 
le passe de donner une semantique denotationnelle de langages 
fonctionnels comme Scheme, presentant un "goto generalise" appele 
capture de continuation (call/cc). Nous montrons que le CPS 
s'etend naturellement, lorsque l'on autorise le non-determinisme 
dans le langage, a un formalisme de transformateur de predicats 
parametres, rappelant les semantiques en arriere de Hoare. 
Independamment du non-determinisme, nous presentons une autre 
idee naive d'extension pour modeliser le parallelisme. L'idee de 
base est d'introduire des echelles de temps locales aux processus; 
ces temps disparaissent ensuite du formalisme, dans la veine des 
semantiques des langages synchrones. La theorie n'est pas developpee, 
seules les idees de depart seront presentees.

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