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 3 janvier, 10h30

                              ---------------
                              Serguei Lenglet
                              ---------------

                           University of Wroclaw

                    ===================================
                    Expansion for universal quantifiers
                    ===================================

Expansion is a tranformation on typings (i.e. on pairs typing environment -
result types) used in intersection types to deduce a typing from an other
one (usually from a principal typing). The definition of this operation has
been made easier by the introduction of expansion variables by Carlier and
Wells in System E. In this talk, we present System Fs, an extension of
system F with expansion variables. We explain how we introduce expansion in
a type system with universal quantifiers, present the main differences
between the expansion in System E and in System Fs, and give the benefits of
this operation in terms of type inference.