To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 30/11/09 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                          Lundi 30 novembre, 10h30

                              ---------------
                              Julien Signoles
                              ---------------

                                    CEA

                 ==========================================
                 Typage dynamique dans un contexte statique
                 ==========================================

Cet exposé présente une bibliothèque fournissant une représentation dynamique
des types OCaml, incluant les instances monomorphes de types polymorphes et
les types abstraits de données. Cette représentation permet de considérer les
types comme des valeurs de première classe. Nous concentrerons notre
présentation sur l'utilisation, l'implémentation et les propriétés de cette
bibliothèque, appelée Type. Cette dernière est incluse dans Frama-C, une
plateforme pour des analyses modulaires de programmes C. En mêlant des
vérifications statiques et dynamiques de types, la bibliothèqe permet de
réduire la distance entre OCaml et les langages dynamiques. Bien que son
implémentation manipule des conversions non sûres de types, l'utilisation de
cette bibliothèque demeure sûre et préserve le résultat de correction forte du
système de types de OCaml. La liaison dynamique et la désérialisation sûre
serviront d'exemples d'utilisation de la bibliothèque au cours de la
présentation.

Dynamic Typing in a Static Setting

This talk presents a library providing a dynamic representation of OCaml
types, including monomorphic instances of polymorphic types and abstract data
types. That allows to consider types as first-class values. We focus on usage,
implementation and properties of this library, called Type, which comes within
Frama-C, a Framework for Modular Analyses of C programs. The library
pragmatically fulfills the gap between OCaml and dynamic languages by mixing
static and dynamic type checking. Its implementation uses unsafe coercions but
its interface is safe: using this library does not break the strong
correctness result of the OCaml type system. Dynamic linkage and safe
unmarshalling are also presented as use cases of the library.