*********************************************************************
*                       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 mars 1995 ********************************************

Rela^che.

*** Vendredi 10 mars 1995 *******************************************

Rela^che.

*** Vendredi 17 mars 1995 *******************************************

Analyse des temps de liaison (Binding-Time Analysis) et Analyse de
ne'cessite' (Strictness Analysis) par interpre'tation abstraite.

Frank VEDRINE (LIENS)

Re'sume' : Dans cet expose', nous montrerons comment integrer dans 
une meme analyse une analyse des temps de liaison ("Binding-Time 
Analysis") et une analyse de ne'cessite', par le biais de 
l'interpre'tation abstraite.
     Le langage utilise' est un petit langage fonctionnel du premier 
ordre, dont la syntaxe ne contient que quelques fonctions de base et
permet des de'finitions re'cursives. L'analyse consiste a` inferrer
des proprie'te's telles que la terminaison su^re, la non-terminaison
su^re et la de'pendance par rapport a` des variables dont nous ne 
connaissons rien. Le principal proble`me rencontre' est le fait que 
mettre la non-terminaison au m^eme niveau que la terminaison (me^me 
si nous arrivons, par souci de pre'cision, a` garder un ordre ou` la 
non-terminaison est le plus petit e'le'ment du treillis) nous oblige 
a` justifier a` la main le passage a` la limite pour nos it'erations
abstraites.

*** Vendredi 24 mars 1995 *******************************************

Rela^che.

*** Vendredi 31 mars 1995 *******************************************

Determination of synchronization and aliasing properties of a
concurrent functional language

Chris COLBY (CMU & LIX)

Re'sume' : We present a framework for the automatic determination of
synchronization and aliasing properties of a functional language
extended with some concurrency constructs from CML.  First, we develop
a semantics in which the usual arbitrary set of channel identifiers is
replaced by a semantic notion of aliasing, and in which the usual
arbitrary set of process identifiers is replaced by a semantic notion
of process history as control path.  The resulting mutual dependency
between synchronization properties and aliasing properties provides a
rich framework for reasoning about these properties.  We then present
an abstract interpretation that isolates regular languages for control
paths and data location paths and uses Deutsch's UP lattices.

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