*********************************************************************
*                       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 mai 1995 *********************************************

Analyse se'mantique de langages synchrones

Thomas JENSEN (LIX)

Re'sume' : Synchronous dataflow languages such as Lustre and Signal
have been proposed as a tool for programming reactive systems. These
languages rely on a clock analysis to ensure that synchronous operations
receive their arguments at the same time. In this talk I will present a
denotational model of a Lustre-like dataflow language and show how a
range of clock analyses for this language can be designed and proved
correct using techniques from abstract interpretation. I will then
give a type system formulation of this analysis using clocks as types
and show how adding polymorphic clocks enables us to treat programs
where clocks vary according to their context. The relationship to the
clock analysis by constraint solving used in the language Signal is
discussed.



*** Vendredi 12 mai 1995 ********************************************

Calculs re'versibles, irre'versibles et optimalite' dans les langages 
fonctionnels (d'apre`s Asperti, Danos, Re'gnier)

Vincent DANOS (Laboratoire de logique, Univ. Paris 7)

Re'sume' : We present a sequential reversible computation scheme for 
lambda-calculus coming from the geometry of interaction (Girard). The 
computation consists in pushing a token along the term (adequately 
represented as a net), each traversal of a node acting reversibly (i.e.,
one-one'ly) on that token.

Then we define an optimization of that scheme taking advantage of its
``call/return'' symmetry that was recently discovered (Asperti, Danos,
Laneve, Regnier). Moves in this case are no longer reversible and 
correspond exactly to the transitions of a simple environment machine
(Krivine's machine).

This result provides a clearcut correspondence between reversible and
irreversible means of computation and provide new insights on the
long-standing problem of optimality.

*** Vendredi 19 mai 1995 ********************************************

Un petit panorama de me'thodes et proble`mes ge'ome'triques en the'orie 
du paralle'lisme

Eric GOUBAULT (LIENS)

Re'sume' : Je tenterai ici d'exposer de facon aussi peu technique que
possible les idees qui sous-tendent certaines methodes geometriques
(HDA, complexes en tout genre, graphes...) qui permettent de decrire
des systemes paralleles (et evidemment aussi des systemes sequentiels)
et de (semi-) decider certains problemes ayant trait a l'ordonnancement
d'actions, l'equivalence semantique par bisimulation, la solvabilite
de problemes de mots...

J'essaierai de montrer pourquoi ces methodes geometriques sont
naturelles pour parler du calcul parallele au sens large (y compris
systemes hybrides...) et de donner un petit catalogue de quelques
theories mathematiques dont les resultats semblent etre parfaitement
adaptes a nos problemes informatiques.

Je terminerai en decrivant quelques problemes non encore resolus,
aussi bien d'ordre mathematique qu'informatique.


*** Vendredi 26 mai 1995 ********************************************

Rela^che

*********************************************************************