*********************************************************************
*                       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 1er decembre 1995 *** 14h00 ****************************

Stackability in higher-order, call-by-value, functional and imperative
programming languages

Anindya BANERJEE (Kansas University & LIX)

Re'sume' : We first consider the simply-typed, call-by-value $\lambda$-
calculus and address the following issues: (1) What it means for such
a language to be implementable with a single, global, stack-based
environment and (2) how the existence of such an environment can be 
predicted statically. The central theme here is the use of the $\lambda$
-abstraction to control the {\em extent} or {\em lifetime} of bindings. 
We identify a subset of the simply-typed, call-by-value $\lambda$-calculus,
where the $\lambda$-abstraction can serve as the block construct for a
stack implementation.

Next, we extend the simply-typed call-by-value $\lambda$-calculus minimally,
to add state. We discuss how such a language can be implemented using a 
stack-based store and how the existence of such a stack-based store can
be predicted statically. Several syntactic block-like constructs for
allocation and deallocation of storage are experimented with. We finally
propose an algorithm for inferring storage blocks in the language.

*** Vendredi 1er decembre 1995 *** 15h00 ****************************

Approximation infe'rieure des e'quations entre termes d'acce`s a` la
me'moire d'un programme

Pavel EMELIANOV (Institut des Syste`mes Informatiques, Novossibirsk
                 & LIX)

Re'sume' : On pre'sente une interpre'tation abstraite qui construit
un invariant qui est une approximation infe'rieure des e'quations
entre termes d'acce`s a` la me'moire d'un programme de type Pascal.
On donne des exemples d'utilisation de l'information produite par
l'analyse pour la de'termination des erreurs a` l'exe'cution et
l'optimisation de programmes.

*** Vendredi 8 decembre 1995 *** 14h00 ******************************

Programming Languages and Dimensions

Andrew KENNEDY (Cambridge University & LIX)

Reporte' au 5 janvier 1996 a 14h30.

*** Vendredi 15 decembre 1995 **************************************

Relache (revue LOMAPS a Pise)

*** Vendredi 22 decembre 1995 **************************************

Relache

*** Vendredi 29 decembre 1995 **************************************

Relache

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