******************************************************************** * LIENS Ecole Normale Superieure * * * * Groupe de travail * * 'Semantique et Interpretation Abstraite' * * P. Cousot * * * * Vendredi, 10h--12h * * Salle W, Toits du DMI, 4eme etage * * DMI ENS 45 rue d'Ulm 75005 Paris * ******************************************************************** *** Vendredi 5 fevrier 1993 *** Relache **************************** *** Vendredi 12 fevrier 1993 *** Seminaire ***10h-12h*** SALLE W *** Un compilateur optimisant de ML vers C. Re'gis Cridlig (LIENS) Since the C language is a machine independent low-level language, it is well-suited as a portable target language for the implementation of higher-order programming languages. This talk will present an efficient C code generator for Caml-Light, a variant of CAML designed at INRIA. Fundamentally, the compilation technique consists of translating ML code via an intermediate language that specifically addresses the compilation of control flow. Thanks to type-safety the runtime system can remain very simple, while the allocation mechanism relies on a new conservative garbage collector. This scheme produces at the same time excellent performance and good portability. It will be soon distributed to be used in conjunction with Caml-Light original byte-code compiler. *** Vendredi 12 fevrier 1993 *** Reunion de travail **************** *** *** 14h -- 16h *********** SALLE ?? *** The Fork Calculus Klaus Havelund (LIENS) *** Vendredi 19 fevrier 1993 *** Reunion de travail **** SALLE W *** Logiques categoriques Eric Goubault (LIENS) *** Vendredi 26 fevrier 1993 *** Relache *************************** *** Vendredi 5 mars 1993 ******* Seminaire ************* SALLE W *** Infe'rence de type pour langages fonctionnels paralle`les. Bruno Monsuez (LIENS) Resume: Dans les extensions paralle`les de ML, les canaux sont for- tement type's. Ils ne peuvent transmettre qu'un seul type de donne'e. En d'autres termes, si un canal a e'te' employe' pour envoyer une variable nume'rique, on devra se restreindre a` n'envoyer que des variables nume'riques par ce dernier. Cependant, une analyse de communication a` la manie`re de Mercouroff permet de de'terminer les communications qui peuvent effectivement se re'aliser entre les divers points d'e'mission et de re'ception d'un programme. Une telle analyse se formule assez simplement dans le formalisme de l'inter- pre'tation abstraite. Comme nous l'avons pre'ce'demment montre', il est possible de construire un syste`me de types polymorphes par interpre'tation abstraite. Dore'navant, nous pouvons combiner ces deux constructions afin de de'finir un syste`me de types autorisant l'existence de canaux ayant un type polymorphe, tout en garantissant la correction du typage. ********************************************************************