********************************************************************* * 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 octobre 1994 ***************************************** Semantics of Binary Choice Constructs Reinhold HECKMANN (Universitaet des Saarlandes, Saarbruecken) Re'sume' : There are several ways to model binary choice constructs in denotational semantics, depending on what information about the results of choice programs is to be represented: 1) Which are the possible results? (set model), or: 2) How often do specific results r occur, counted by the number of different traces leading to r? (multiset model), or: 3) What is the probability for some specific result, if every choice is performed by tossing an unbiased coin? (probabilistic model) *** Vendredi 14 octobre 1994 **************************************** Set-Based Program Analysis Nevin HEINTZE (Carnegie Mellon University) Re'sume' : In set-based analysis (SBA), programs are approximated using a very simple abstraction: programs variables are viewed as sets of values. In essence, this corresponds to ignoring inter-variable dependencies, but making no approximation of the underlying space of values. One advantage of the SBA approach is that it provides an intuitive, abstract and non-algorithmic view of what the analysis will achieve, in combination with an accurate and uniform treatment of data-structures. While SBA can be formulated as an abstract interpretation, the corresponding iterative fixpoint computation does not terminate. Instead, new algorithmic techniques are needed to reason directly about (arbitrary) sets of values. For this purpose, we have developed the calculus of set constraints. I will describe the application of SBA to a variety of languages, and give details of implementations (including a recent one for full ML, involving exceptions, arithmetic, arrays and continuations). *** Vendredi 21 octobre 1994 **************************************** The Geometry of implementation Ian MACKIE (Imperial College & LIX) Re'sume' : In this talk I will present the Geometry of Implementation - an implementation technique for functional programming languages based on Girard's Geometry of Interaction semantics for Linear Logic. A simple functional language (PCF) is first compiled into Linear Logic proof structures which will be the starting point of all our ideas. We begin with the basic machine which is simply a computational interpretation of the Geometry of Interaction. This yields a compilation of PCF directly into assembly language. The resulting code produced is very compact, and requires a very small run-time system. The simplicity of this compilation is offset by poor performance. A simple analysis of the semantic foundation leads to a series of optimisations that we will outline that require only a slight modification of the compiler. Finally, we hint at some connections with existing implementations so that we are in a position to talk about the efficiency of this compilation technology. *** Vendredi 28 octobre 1994 **************************************** N\'egation constructive par \'elagage pour les langages CLP et CC Francois FAGES (LIENS) Re'sume' : Nous montrons qu'un me'canisme simple d'elagage concurrent entre arbres standards de de'rivation SLD, appele' ne'gation constructive par e'lagage, suffit a` doter les programmes logiques avec contraintes normaux d'une se'mantique ope'rationnelle correcte et comple`te vis a` vis de la se'mantique de'clarative en logique tri-value'e de Fitting et Kunen. Nous pensons que ce sche'ma est suffisament simple pour conduire a` des imple'mentations pratiques, car le principe d'e'lagage concurrent est la seule extension ne'cessaire au traitement de la ne'gation. On e'tudie une version finitaire continue de l'ope'rateur de Fitting, et on montre que la se'mantique de point fixe correspondante est ``fully abstract'' pour l'observation des contraintes re'ponses calcule'es. Dans le contexte des pre'dicats d'ordre supe'rieur d'optimisation, qui sont courament utilise's dans les syste`mes CLP et qui peuvent s'exprimer avec une formule logique avec ne'gation, nous montrons que la ne'gation constructive par e'lagage se spe'cialise en une proce'dure efficace de type ``se'paration- e'valuation'', prouve'e correcte et comple`te sans restriction sur le degre' d'imbrication et le degre' de re'cursion a` travers les pre'dicats d'optimisation. *********************************************************************