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

*** Vendredi 2 fevrier 1996 **** 14h00 ******************************

Interaction Nets with State

Ian MACKIE (LIX)

Re'sume' :  In this talk I will present a system of interaction, based
on Lafont's interaction nets, which incorporates a notion of state. This
allows us to write nets for larger classes of term rewriting
systems, genuine parallel functions, non-determinism, communication,
sharing, and can be used to code features from Standard ML and
Concurrent ML.

This is joint work with Maribel Fernandez (ENS)

*** Vendredi 9 fevrier 1996 **** 14h00 ******************************

Relache (voir le groupe de travail sur
http://www.ens.fr/~cousot/annoncegdtravail.html).

*** Vendredi 16 fevrier 1996 **** 14h00 *****************************

Logiques non classiques, preuves uniformes et BDDs

Jean GOUBAULT (Bull)

Re'sume' : Les BDDs (diagrammes de decision binaire) sont
des structures informatiques simples fournissent des methodes
efficaces de resolution de problemes de decision en logique
propositionnelle classique, notamment celui de la satisfiabilite.
Mais ils sont intimement lies au tertium non datur de la logique
classique.

        Le but de cet expose est de montrer qu'une variante
des zero-suppressed BDDs de Minato est tout ce dont on a
besoin pour representer des calculs de sequents dans des
logiques, classiques ou non-classiques.  Les BDDs non-classiques
qui en resultent seront alors d'autant plus utilisables qu'un
maximum de preuves dans le calcul des sequents correspondant
peuvent etre presentees sous un format uniforme --- une notion
due a Scedrov, Miller et d'autres.
        J'essaierai de justifier le slogan selon lequel les BDDs
non-classiques sont une facon d'implementer une forme de
parallelisme SIMD sur une machine sequentielle, dans le cas
de recherche de fragments uniformes de preuves.

        Des connaissances de base sur le calcul des sequents,
la methode des tableaux, et les BDDs aideront beaucoup a la
comprehension de l'expose.


*** Vendredi 23 fevrier 1996 **** 14h00 *****************************

On describing quantitative aspects of mobile processes: distributed
environments and timing

Pierpaolo DEGANO (Universite' de Pise)

Re'sume' : We proposed enhanced operational semantics for concurrency.
The basic model are {\em proved transition systems}. Their transitions are
labelled by encodings of their proofs, implementing the motto {\scriptsize
TRANSITIONS AS PROOFS}.
Then, simple relabellings yield the main semantics presented in the
literature, and their comparison is reduced to compare their
relabelling functions. In particular, we studied the so-called {\em truly
concurrent} semantics, that express aspects like causality and locality.

Here, we discuss how proved transition systems are capable to express also
quantitative aspects of concurrent processes, besides the behavioural ones
mentioned above. The study is carried out considering mobile processes
expressed in $\pi$-calculus.
First, we will discuss the problem of specifying {\em local} handlers for
the environments of processes, thus taking architectural constraints into
account.
Then, we will sketch how the performance of mobile processes can be
analysed by enriching them with time information.


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