********************************************************************* * Ecole Normale Superieure * * * * Seminaire * * 'Semantique et Interpretation Abstraite' * * P. Cousot * * * * Vendredi, 14h--16h * * Salle W, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 15 octobre 1993 **************************************** Types fractionnels Bruno MONSUEZ (LIENS) Re'sume' : Le syst\`eme de types d'Hindley/Milner souffre de certaines limitations. En effet toutes les expressions ML n'ont pas leur type le plus g\'en\'eral possible et certaines expressions n'ont m\^eme pas de type tout simplement. Par exemple, l'expression $\lambda x.xx$ n'est pas typable. Coppo et Dezani ont d\'efini un syst\`eme de types bien plus g\'en\'eral que celui de ML. Dans ce syst\`eme de types, toutes les expressions ayant une forme normale de t\^ete sont typables. Par exemple, dans ce syst\`eme de types, l'expression $\Delta = \lambda x.xx$ est typable et poss\`ede comme type $(\alpha \cap (\alpha \ra\beta)) \ra \beta$. Toutefois, ce syst\`eme est si g\'en\'eral que le type principal n'est pas calculable dans le cas g\'en\'eral. Dans un autre domaine, Didier R\'emy propose d'adapter la notion de << Projection Types >> aux typages de monstres comme $\Delta$. Dans son mod\`ele, le combinateur $\Delta$ \`a le type $[a~:~\tau\ra \sigma;~b~:~\tau] \ra\sigma$, mais cela n\'ecessite de transformer syntaxiquement l'expression $\lambda x.xx$ en $\lambda x.x/a~x/b$. Lors de l'expos\'e, nous proposerons une extension de l'alg\`ebre des types construite \`a partir de l'interpr\'etation abstraite et telle que des termes comme $\Delta$ ou m\^eme $\Delta \Delta$ soient typables et dont le type principal bien entendu est syst\'ematique- ment calculable. *** Vendredi 22 octobre 1993 **************************************** Horloges vectorielles et re'exe'cution distribue'e. Fre'de'ric RUGET (Chorus) Re'sume' : CDB est un de'bogueur permettant de "rejouer" des exe'cu- tions pre'alablement enregistre'es d'applications distribue'es tournant au dessus du syste`me Chorus. Une application a` rejouer consiste en un ensemble dynamique d'objets re'partis sur diffe'rents sites. CDB est compose' d'un module par site, qui contro^le les objets locaux de l'application. Mais chaque module a aussi besoin d'une connaissance globale des objets pre'sents sur les autres sites. Nous montrerons comment une telle connaissance peut e^tre obtenue de facon efficace en utilisant des horloges vectorielles. Si le temps le permet, nous montrerons que l'utilisation d'horloges vectorielle allie'e a` une technique d'estampillage d'historiques permettrait me^me aux modules de CDB d'avoir une connaissance suffisamment pre'cise des objets pre'sents sur les autres sites pour pouvoir restituer l'e'tat d'un site apre`s un crash. *** Vendredi 29 octobre 1993 **************************************** Linear Logic and implementations of the lambda-calculus. Ian MACKIE (Imperial College/LIX) Re'sume' : I will present three ways of implementing the lambda calculus using ideas from Linear Logic, by translating the lambda calculus into Linear Logic proof structures. The emphasis will be on using ideas of Linear Logic and Optimal Reduction to give new and (maybe) more efficient implementations of the real functional programming languages. First a graph reduction algorithm which is a variant of the work by Gonthier, Abadi and Levy on optimal reduction. The algorithm presented is NOT optimal, but will do far less work in terms of number of interactions. The proof of correctness of this algorithm is performed by using ideas from Girard's Geometry of Interaction semantics for Linear Logic. The proof technique used for the graph reduction algorithm can be used as an implementation itself. This leads to a token passing implementation of the lambda calculus: a token travelling around a fixed network. I will discuss implementation issues and efficiency. Finally, a controlled graph reduction algorithm will be mentioned which will borrow ideas from the previous two algorithms to give the best of both worlds! *********************************************************************