*********************************************************************
*                       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 4 novembre 1994 ****************************************

Static and Dynamic Processor Allocation for Higher-Order Concurrent 
Programs

Flemming NIELSON (DAIMI, AArhus)

Re'sume' : Concurrent ML (CML) is an extension of the functional 
language SML with primitives for the dynamic creation of processes 
and channels and for communication of values over channels. To obtain 
efficient implementations it is necessary to exploit information 
about the communication structure of programs but while perhaps 
apparent to the programmer such information is not normally available 
to the compiler. Hence program analyses that can provide information 
about the communication structure are in strong demand.

In this talk we show how a polymorphic type system for SML can be
extended to produce not only the types of CML programs but also their
communication behaviour expressed as a term in a process algebra
designed to suit CML.  Starting from the process algebra we then
develop two analyses that facilitate the intelligent placement of
processes on processors. Both analyses are obtained by augmenting an
inference system for counting the number of channels created, the
number of input and output operations performed, and the number of
processes spawned by the execution of a CML program (as recorded by a
term in the process algebra). One analysis provides information useful
for statically determining for each fork operation on which processor
all spawned processes should reside, whereas the other provides
information useful for dynamically deciding for each newly spawned
process which processor it should reside on.

This is joint work with Hanne Riis Nielson.

*** Vendredi 11 novembre 1994 ***************************************

Rela^che.

*** Vendredi 18 novembre 1994 ***************************************

Uniform PERs and comportment analysis

Alan MYCROFT (Cambridge University & LIX)

Re'sume' : We define the notion of 'uniform PER' as which comprises
those PERs invariant under the set of bottom-preserving permutations
at ground types and hereditarily at higher types.

We show that such PERs describe all example notions of comportment 
analysis introduced by the Cousots (1994) which was itself introduced 
to group together the various 'strictness-like' properties.  Further 
properties emerge leading to 7 uniform properties on int, and 14 on 
int->int.

Uniform PERs (or subsets thereof) can be taken as a space of abstract 
values for abstract interpretation in the style of Nielson.

*** Vendredi 25 novembre 1994 ***************************************

A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.

Nick BENTON (Cambridge University)

Re'sume' : This talk will describe the connection between intuitionistic
linear logic and ordinary intuitionistic logic by giving a
logic, term calculus and categorical model for a system in which
the linear and non-linear worlds exist on an equal footing, with
operations allowing one to pass in both directions. We start
from the categorical model of ILL given by Benton, Bierman,
Hyland and de Paiva and show that this is equivalent to having a
symmetric monoidal adjunction between a symmetric monoidal
closed category and a cartesian closed category. We then derive
both a sequent calculus and a natural deduction presentation of
the logic corresponding to the new notion of model.


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