*********************************************************************
* 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.
*********************************************************************