*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                           Salle S16, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************


*** Vendredi 6 janvier 2005 *****************************************

Pierre-Lo"ic Garoche (ENSEEIHT)

Type systems vs. Abstract Interpretations

Abstract: 

We focus here on the verification of mobile systems described by process        
calculi, in particular, by an actor calculus.                                   
                                                                                
The actor model was introduced in 87 by Agha. This model, based on a            
network of autonomous entities, communicating via an asynchronous               
protocol by sending labeled messages, is suited to represent concurrent         
objects. CAP, a Primitive Actor Calculus, is one of those calculi. We           
are interested to infere properties about mobile systems described in           
this formalism such as linearity (not more then one "actor" on a                
channel), stuck-freeness or to bound the system.                                
                                                                                
We will present the two following approaches to infere those properties:        
(1) behavioral type systems. With a denotational and more data-flow             
oriented point of view, we present type systems, similar to those of            
Kobayashi, Yonezawa or Ravara, intended to capture behavioral                   
properties, but without any type annotation;                                    
                                                                                
(2) abstract interpretations. With an operational and more control-flow         
oriented conceit, we present how we express CAP into the generic                
framework of J. Feret.                                                          
                                                                                
Finally, we will compare those two guidelines and discuss which kind of         
properties, and how, could be captured by each framework.                       

*********************************************************************
Pour recevoir l'annonce par courrier electronique: 
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************