*********************************************************************
*                       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 26 novembre 1993 ***************************************

Constraint Logic Programming over Finite Domains

Philippe CODOGNET (INRIA-Rocquencourt)

Re'sume' : Constraint Logic Programming (CLP) has shown to be a very
active field of research over recent years, and languages such as 
CHIP, CLP(R) and Prolog III have proved that this approach opens 
Logic Programming (LP) to a wide range of real-life applications, by
combining both the declarativity of Logic Programming and the ability
to reason and compute with partial information (constraints) on 
specific domains. Among the many domains already investigated, the
most successful are certainly finite domains, because they can be
used in most applications and there exists efficient methods for
solving these constraints. We will briefly review traditional methods
and present the solver used in our clp(FD) compiler, which is based
on the ``glass-box'' paradigm, as opposed to the ``black-box'' 
approach of CHIP. Several extensions will also be proposed, such as
boolean constraints and complex constraints. New areas such as 
reactive constraint solving and concurrent constraint languages
will be presented, and the interest of the glass-box approach in 
those domains will be argued.

*** Vendredi 10 de'cembre 1993 **************************************

Compositional and Abductive Analysis of Modular Logic Programs

Roberto GIACOBAZZI (LIX, E'cole Polytechnique)

Re'sume' : We describe a semantic basis for a compositional approach 
to the analysis of logic programs.  A logic program is viewed as 
consisting of a set of modules, each module defining a subset of the 
program's predicates.  Analyses are constructed by considering 
abstract interpretations of a compositional semantics. The abstract
meaning of a module corresponds to its analysis and composition of 
abstract meanings corresponds to composition of analyses.  Such an 
approach is essential for large program development so that altering
one module does not require re-analysis of the entire program.
We show that for a substantial class of analysis, compositional
analyses that are based on a notion of "abstract unfolding" provide
the same precision as non-compositional ones.

The same abstract semantics for composition provides also a sound
framework for "abstract abduction".  The standard analysis of logic
programs is typically intended to statically derive approximated
information (the analysis) about run-time properties of programs,
by applying rules (clauses) to particular cases (goals), with the
inference of a result.  In the compositional analysis framework this
"deductive" process corresponds precisely to iterate the unfolding
of clauses with particular definitions for their extensional part.
These definitions can either be assumed imported from other modules
(open) or be part of the deduction itself.  The converse of this
process, i.e. "abductive" analysis, consists in inferring the
possible extensions for undefined (imported) predicates of a module
by assuming a given property on the result of the composition.
The abductive analysis is particularly useful for the systematic
development of modular logic programs by statically generate
(abstract) specifications for modules.  This because in many cases
the applicability of optimization techniques to a program module may
depend on the definition of its imported predicates.

Compositional and abductive analyses for ground dependencies are
included to illustrate the approach.

Joint work with: M. Codish and S.K. Debray

*** Vendredi 17 de'cembre 1993 **************************************

A Refinement Logic for the Fork Calculus (Towards a Logic for 
Concurrent ML)

Klaus HAVELUND (LIX, E'cole Polytechnique)

Re'sume' : The Fork Calculus, FC, represents a theory of concurrency.
It is in family with CCS, but differs in the  way that  processes are
put in parallel. In CCS there is a binary parallel operator $|$, and
two  processes p and q are put in parallel by p|q.  In FC there is a
unary "fork" operator, and a process p is activated to ``run in 
parallel with the rest  of the program''  by fork(p).  We provide FC
with an  operational  semantics, together with a congruence relation
between processes.  We further present a variant of Hennessy-Milner 
modal logic for the calculus.  The logic is a refinement logic in the
sense that the programming constructs of FC themselves are operators
in the logic. FC has been developed during an investigation of the 
programming language CML (Concurrent ML), an extension of ML with 
FC-like concurrency primitives. The goal is to obtain a logic for 
CML.

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