*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                 Salle W, 4e`me e'tage, toits du DMI               *
*                 DMI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 3 janvier 1997 **** 14h00 *****************************

Rela^che

*** Vendredi 10 janvier 1997 **** 14h00 ****************************

Rela^che

*** Vendredi 17 janvier 1997 **** 14h00 ****************************

Rela^che (POPL'97, voir http://lix.polytechnique.fr/~radhia/popl97/)

*** Vendredi 24 janvier 1997 **** 14h00 ****************************

Continuations and threads
    Expressing machine concurrency directly in advanced languages

Olin SHIVERS (MIT)

Re'sume': It is well known [Wand] that concurrency can be expressed within 
languages that provide a continuation type.  However, a number of misconceptions
persist regarding the relationship between threads and continuations.  I
discuss the proper relationship between these two objects, and present a
model for directly expressing concurrency using continuations.  The model
is designed to support systems programming, and has several novel
features: it is synchronous, preemptible, and fully virtualisable,
allowing schedulers to be written by unprivileged users that are
indistinguishable from top-level schedulers that actually control access
to the hardware resources.

Note: le se'minaire de Corrado PRIAMI (Enhanced Operational Semantics 
for Concurrency) est reporte' au Vendredi 7 fe'vrier 1997.

*** Vendredi 31 janvier 1997 **** 14h00 ****************************

On deciding non-interleaving bisimulations

Pier Paolo DEGANO (Universite' de Pise, invite' ENS)

Re'sume' : We propose a new way of checking non-interleaving bisimulations
on (suitably enriched) transition systems, by reducing it to a sort of
interleaving bisimilarity check.  This is done for a large variety of
non-interleaving bisimulation (roughly speaking, for all those that are
preserved by unfolding transition systems).

The basic idea is to have a linearized, incremental representation of the 
non-interleaving aspects occurring in a computation of transition systems 
(cf. how causality is encoded in causal trees).
This reduces the check for non-interleaving bisimilarity to a possibly 
more expensive check, yet interleaving in style.
Now, suppose you wish to check that two given transition systems S1 and S2
are in a specific non-interleaving bisimulation R.
First, build a (finite) interleaving bisimulation S. 
Secondly, unfold S1 and S2 until the two trees T1 and T2 you obtain 
have maximal depth k, which is determined by S.
Finally, T1 R T2 if and only if S1 R S2.

The last statement implies that if a given interleaving bisimulation
(resistent to unfoldings) is decidable, then its non-interleaving versions
are such.

Joint work with Corrado Priami

*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr
WWW: http://www.ens.fr/~cousot/annonceseminaire.html
*********************************************************************