To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 20/04/07 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.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

                           Vendredi 20 avril, 14h

                   -------------------------------------
                   Jérôme Vouillon et Paul-André Melliès
                   -------------------------------------

                                    CNRS

      ================================================================
      Une approche sémantique et modale du typage des langages machine
      ================================================================

Nous présenterons un modèle sémantique des types récursifs et polymorphes avec
références mutables. Nous y interprèterons tous les constructeurs de type
utilisés pour le typage des programmes en langage machine issus de la
compilation des langages fonctionnels. Nous établirons dans ce cadre purement
sémantique un théorème de correction du système de type -- assurant que tout
programme bien typé est sûr. Le modèle s'exprime naturellement à l'aide d'une
sémantique de Kripke vérifiant l'axiome de Gödel-Löb, introduit en logique de
prouvabilité.  Nous expliquerons brièvement quelles caractéristiques logiques
de Coq ont été utilisées pour la démonstration validée du résultat.