Actualités du LIPN

Le 15 novembre 2010, à 15h30 en salle B311, le séminaire LCR accueille Paolo Tranquilli (LIP, ENS Lyon).

Je présenterai un travail en collaboration avec Giulio Manzonetto qui montre la normalisation forte d’MLF par une simulation dans le système F. MLF est une extension conservative de ML qui permet de programmer tous le termes du système F à l’aide d’annotations partielles de type. Dans une première partie je vais décrire MLF, et notamment xMLF, sa variante explicite en style Church. Dans xMLF les relations d’instance des types sont explicitement notés par des entités nommées "instantiations" qui jouent en fait un rôle de coercitions et qui se réduisent de façon non triviale. Pour mieux raisonner sur ces aspects de xMLF on va le traduire dans une décoration du système F, le calcul de coercitions Fc, qui abstrait le mécanisme de coercition. On va donc présenter ce calcul et montrer que l’effacement des coercitions qui plonge Fc dans le lambda calcul ordinaire est une bisimulation faible. Finalement on va définir la traduction de xMLF dans Fc et utiliser la bisimulation pour montrer la normalisation forte des autres variantes de MLF aussi.