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