*********************************************************************
* 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 mars 1994 ********************************************
Semi-Unification
Assaf J. KFOURY (Boston University)
Re'sume' : Let T be the set of all terms built up from a finite set of
function symbols F = { f_1,...,f_k }, each with a fixed arity, and a
(possibly infinite) set of variables X = { x_0, x_1, x_2, ... }. An
"instance" I of semi-unification is a finite set of n > 0 pairs of
terms in T:
I = { (t_1,u_1), ... , (t_n,u_n) }
As usual, a "substitution" is a function S from X to T, extended to a
function from T to T. A substitution S is a "solution" of the instance
I iff there are substitutions S_1, ... , S_n such that:
S_1(S(t_1)) = S(u_1) , ... , S_n(S(t_n)) = S(u_n)
The Semi-Unification Problem (SUP) is the problem of deciding, for an
arbitrary instance I, whether I has a solution.
Semi-unification has emerged as a new area of study in theoretical
computer science since 1988, with various applications in several
branches of computer science and mathematical logic (proof theory,
computational linguistics, term-rewriting, database theory, polymor-
phic type systems). Various forms of SUP have been formulated, based
on restrictions and/or extensions of the set of terms T, and on the
number of pairs in an instance I and possible connections between
these pairs. We present decidable cases of the problem (with their
complexity), undecidable cases, and cases still to be resolved.
In the last 3 years, the most striking successes have been in type
theory, specifically, in solving long-standing open problems of
type-reconstruction for polymorphically typed lambda-calculi and
functional programming languages. We discuss the significance of
these results for the development of modern programming languages.
We review some of these applications.
*** Vendredi 11 mars 1994 *******************************************
Total Correctness and Improvement in the Transformation of Recursive
Programs
David SANDS (DIKU, Copenhague)
Re'sume' : The goal of program transformation is to improve efficiency
while preserving meaning. One of the best known transformation
techniques is Burstall and Darlington's unfold/fold method. This
approach has been used extensively, and many transformations can be
viewed as instances of this method. Unfortunately the unfold/fold
method itself guarantees neither improvement in efficiency nor
total-correctness of the resulting programs.
This talk presents a semantic condition for the total correctness of
transformations on recursive programs, which deals with higher-order
functional languages (both strict and non-strict) including lazy data
structures.
The condition in question makes essential use of a formalised
improvement-theory; as a rather pleasing corollary, it also guarantees
that the transformed program is a formal improvement over the
original. The condition appears to be useful and practical; this is
illustrated in the context of the unfold/fold method. A simple
annotation is introduced, whose meaning and algebraic properties are
given by the improvement theory. It is shown how transformation steps
can be extended with annotations so as to guarantee, simultaneously,
total correctness and efficiency improvement in the resulting
programs.
*** Vendredi 18 mars 1994 *******************************************
Model-checking et programmation logique avec contraintes,
un rapprochement utile
Marc-Michel CORSINI (LABRI, Bordeaux)
Re'sume' : Nous pre'sentons le langage de contraintes Toupie qui est un
interpre'teur de mu--calcul sur les domaines finis. Les langages de
contraintes sur les domaines finis qui appartiennent a` la famille
des CLP(FD), ont pour but de chercher une solution a` un ensemble de
contraintes, e'ventuellement la meilleure suivant un certain crite`re.
En Toupie, les contraintes sont utilise'es pour caracte'riser les
relations existant entre variables. Nous de'montrons que notre approche
permet de trouver des solutions a` des problemes difficiles qui ne
peuvent e^tre re'solus avec un langage de la famille CLP(FD).
*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************