********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h30--16h * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 5 janvier 1996 **** 14h30 ****************************** Programming Languages and Dimensions Andrew KENNEDY (Cambridge University & LIX) Re'sume' : Scientists and engineers must ensure that the equations which they use are dimensionally consistent, but existing programming languages treat all numeric values as dimensionless. In this talk I will discuss the extension of programming languages to support the notion of physical dimension. A type system will be presented similar to that of the programming language ML but extended with polymorphic dimension types. Most general dimension types can be deduced automatically by an inference algorithm. A semantics for the language is used to show that "well-dimensioned programs do not go wrong" and also that a "dimensional invariance theorem" holds for programs with dimension types: this captures the idea that evaluation is independent of the units of measure used. *** Vendredi 12 janvier 1996 *** 14h30 ****************************** Interaction Categories: A Theory of Types for Concurrency Simon GAY (Imperial College, Londres) Re'sume' : The theory of interaction categories was proposed by Samson Abramsky, and has been developed further in collaboration with the speaker and Raja Nagarajan. It provides a semantic foundation for typed concurrency, formulated in terms of category theory: objects are types (specifications), morphisms are processes satisfying those specifications, and composition is interaction. The simplest interaction categories have types corresponding to rudimentary safety specifications; others have more complex types which specify more interesting properties such as deadlock-freedom. In general, the typed process construction rules arising from the categorical structure are seen as compositional proof rules for the properties in question. This talk will present a general overview of interaction categories - defining the basic examples, presenting some of the applications (typed process calculi; a type-based approach to verification of concurrent systems) and discussing future directions. *** Vendredi 19 janvier 1996 *** 14h30 ****************************** S\'emantiques vraiment parall\`eles de CML et Interpr\'etation Abstraite Re'gis CRIDLIG (LIENS) Re'sume' : Une nouvelle s\'emantique de Concurrent~ML bas\'ee sur des syst\`emes de transitions de dimension sup\'erieure sera pr\'esent\'ee et compar\'ee aux s\'emantiques d\'ej\`a propos\'ees pour ce langage. Tout en restant op\'erationnelle par nature, cette s\'emantique permet de mod\'eliser les ex\'ecutions asynchrones d'op\'erations parall\`eles~: un automate (HDA) est construit \`a partir de l'\'etat initial du programme en ajoutant de nouvelles transitions petit-pas \`a partir des \'etats d\'ej\`a pr\'esents, dans le style SOS. Une r\`egle particuli\`ere qui tient compte des communications le long des canaux b\^atit les transitions de dimension sup\'erieure \`a partir de transitions sans interf\'erence. Les r\`egles s\'emantiques d\'efinissent ainsi un syst\`eme de transitions comprenant toutes les actions survenant en parall\`ele lors de l'ex\'ecution d'un programme. En deuxi\`eme lieu nous montrerons comment d\'efinir des mod\`eles finitaires de cette s\'emantique standard par la m\'ethode d'interpr\'etation abstraite. D'une part une interpr\'etation abstraite {\em sup\'erieure} couvre un sur-ensemble de tous les \'etats et aussi des transitions s\'equentielles et parall\`eles pouvant exister dynamiquement. D'autre part une approximation {\em inf\'erieure} d\'efinit un sous-ensemble des \'etats et des transitions pr\'esents dans la s\'emantique standard. Une abstraction {\em duale}, bas\'ee sur ces approximations sup\'erieure et inf\'erieure, sert alors \`a calculer un automate abstrait sur lequel on peut automatiquement v\'erifier des propri\'et\'es statiques exprim\'ees dans une logique modale universelle et existentielle. On pourra donc par cette m\'ethode v\'erifier toute une classe de sp\'ecifications formelles qu'un programme CML doit supporter. *** Vendredi 26 janvier 1996 *** 14h30 ****************************** Comparing Geometry of Interaction and Environment Machines Bruno BLANCHET (ENS) & Ian MACKIE (LIX) Re'sume' : In this talk we fist recap on the basic ideas of the Geometry of Interaction Machine and show how it can be optimised to relate to more traditional environment machines (e.g. Krivine). We then extend this to a small functional language (a subset of CAML) and discuss the implementation issues involved. An analysis of benchmark results follows which shows a surprising result that the GOI Machine performs better in general. We then look at some other variants of the Krivine Machine and other evaluation strategies which shows that the GOI machine is still very far from a usable implementation technique. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.ens.fr/~cousot/annonceseminaire.html *********************************************************************