To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 17/03/08 - 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

                            Lundi 17 mars, 10h30

                              ----------------
                              Sylvain Lebresne
                              ----------------

                             Université Paris 7
                           et École Polytechnique

                 =========================================
                 Un système d'exceptions pour le Système F
                 =========================================

Les exceptions sont généralement vues comme un mécanisme modifiant le
flot de contrôle d'un programme. Cette vision cantonne les exceptions
aux langages pour lesquels la notion de flot de contrôle est bien
définie, ce qui n'est généralement pas le cas pour les langages de la
théorie des types.

Nous présenterons un mécanisme où les exceptions sont attachées aux
valeurs plutôt qu'au flot de contrôle, ainsi qu'un système de types pour
ces exceptions basé sur la notion de corruption. Nous montrerons que
cette notion, utilisée à travers une relation de sous-typage, permet la
détection statique d'exceptions non rattrapées, et ce sans compromettre
la propagation automatique des exceptions.

Nous illustrerons ce système d'exceptions dans le cadre d'une extension
du Système F, utilisé ici comme une première étape vers des systèmes de
types plus riches (avec pour horizon le calcul des constructions).

Enfin, nous présenterons un modèle de réalisabilité pour justifier
et expliquer la notion de corruption dans notre calcul.