********************************************************************* * 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 5 novembre 1993 **************************************** Lambda-mix: a Self-applicable Partial Evaluator for the Lambda Calculus Neil D. Jones (DIKU, Universite' de Copenhague) Re'sume' : Partial evaluation is an automatic program transformation technique: given a two input program {\tt p} and a value {\tt in1} of its first input, a partial evaluator will return a {\em specialized} program {\tt p}$_{\tt in1}$. This has the property that, if {\tt p}$_{\tt in1}$ is applied to any value {\tt in2} of {\tt p}'s second input, it will yield the same result that {\tt p} would have yielded on both inputs. The motivation is efficiency: {\tt p}$_{\tt in1}$ may be much faster than {\tt p}. The talk describes a simple partial evaluator for a higher order language, the untyped lambda calculus, and is joint work with Carsten Gomard. An example shows how a partial evaluator can be used automatically to compile a source language, given as input a language definition in the form of an lambda expression as used in denotational semantics. Further, self-application makes it possible to generate a compiler from an interpreter. The goal was to generalize the techniques that worked well for first order to include more expressive higher order languages. Binding times in data and controlare separated using a two-level lambda calculus syntactically similar to those of Nielson and Nielson, and simpler than those used in earlier partial evaluators. A key idea is the application of type inference to an untyped language (!). Some language-independent principles and techniques for partial evaluation are described, ending with an overview of some existing partial evaluation systems for higher-order languages. *** Vendredi 12 novembre 1993 *************************************** Spe'cification de sSyste`mes de transition avec ne'gation Re'mi LISSAJOUX (Thomson-LCR) Re'sume' : On pre'sente une me'thode pour de'finir des se'mantiques ope'rationnelles structure'es (SOS) a` la Plotkin e'tendues avec la ne'gation (une transition est possible si une autre transition est impossible). La ne'gation dans les SOS permet entre autres de de'finir des syste`mes de transitions avec priorite's. On montre comment, des crite`res syntaxiques simples base's sur une extension de la notion de re'cursion garde'e permettent de garantir l'existence et l'unicite' d'un mode`le de la SOS e'tendue. On montre e'galement que les me^mes crite`res assurent que la bissimulation est une congruence. Enfin, on compare notre formalisme a` ceux de J.F. Groote (dont c'est une spe'cialisation) et B. Bloom (GSOS). *** Vendredi 19 novembre 1993 *************************************** Compositional Reasoning about Concurrent Processes Thomas JENSEN (LIX - E'cole Polytechnique) Re'sume' : In this talk I shall address the issue of how to construct a formal system for reasoning about concurrent processes in a compositional manner. It has been known for a long time that the usual Hoare-style logics for sequential languages do not extend easily to languages with parallel constructs. Brookes has introduced a notion of transition assertions to overcome this deficiency. I will present transition assertions and provide some examples of how these can express properties of labelled transition systems. I will then show how to define operators on transition assertions that safely models sequential and parallel composition of transition systems and discuss some of their applications. *********************************************************************