*********************************************************************
*                       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 7 janvier 1993 *****************************************

A new scheme based on pruning for constructive  negation  in  CLP
and CC languages

Francois FAGES (LIENS)

Re'sume': Because of their importance in real-life  applications,
most  constraint  logic programming systems, such as CHIP, CLP(R)
and Prolog III, include various higher-order predicates  for  op-
timization.  These constructs do not belong however to the formal
framework of Jaffar and Lassez and they lack a declarative seman-
tics.   In this talk I shall present an approach based on the se-
mantics of negation. Constructive negation  and  its  compilative
version  named  intensional negation, provide already correct and
complete schemes w.r.t. the 3-valued interpretation of logic pro-
grams  with negation.  But these rules are not easily amenable to
practical implementations.  A new  scheme  based  on  pruning  in
CSLD-derivation  forests  will be proposed and proved correct and
complete w.r.t. the 3-valued completion of the program.  We shall
derive  from  that  scheme a family of branch and bound like pro-
cedures for optimization that  can  be  practically  implemented.
Following  the  same line of development we shall also outline an
extension of the CC family of languages with negation, and of its
denotational semantics defined by non-linear closure operators.

*** Vendredi 14 janvier 1993 ****************************************

Improving Abstract Interpretations with Continuations

Juarez Assumpcao MUYLAERT-FILHO (Imperial College, Londres)

Re'sume' : In this talk we consider the benefits of continuations for
abstract interpretations (a.i.) of programs written in simply-typed
(lazy) functional languages. The a.i. framework we consider was first
described in [BHA85] and uses finite domains. The idea is to do
abstract interpretation of continuised terms. The basic slogan is
continuations do improve abstract interpretations as they expose more
properties that were otherwise hidden in the untranslated programs.

[BHA85] Burn, Hankin and Abramsky, The Theory of
Strictness Analysis for higher-order functions,
LNCS 217, 1985.

*** Vendredi 21 janvier 1993 ****************************************

Rela^che.

*** Vendredi 28 janvier 1993 ****************************************

Proving Concurrent Constraint Programs Correct

Maurizio GABBRIELLI (CWI, Amsterdam)

Re'sume' : We develop a compositional proof-system for proving the 
partial correctness of concurrent constraint programs (ccp). We first
introduce a specification logic to reason about the correctness of
ccp programs in terms of properties of constraints. The rule of the
calculus are then obtained by ``mirroring'' the equations of a simple
denotational semantics which describes the strongest postcondition of
a ccp process.

Our results clarify the declarative nature of ccp since allow to 
consider a ccp program as a theory in the specification logic. The
operators of the language are interpreted logically  by considering
action prefixing as implication, non-deterministic choice as 
disjunction and parallel composition as conjunction.

Joint work with F.S. de Boer, E. Marchiori and C. Palamidessi.

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