To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Cristal - 17/02/06 - Paris - FR

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

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

                         Vendredi 17 fevrier, 10h30

                             -----------------
                             Sébastien Carlier
                             -----------------

                           Heriot-Watt University

         =========================================================
         Expansion: Connecting Intersection Types, Type Inference,
                 Principal Typings, Interaction Nets, etc.
         =========================================================

The operation of _expansion_ on typings was introduced at the end of
the 1970s by Coppo, Dezani, and Venneri for reasoning about the
possible typings of a term when using intersection types.  Until
recently, expansion has remained somewhat mysterious and unfamiliar,
even though it is essential for carrying out _compositional_ type
inference.

The fundamental idea of expansion is to be able to calculate the
effect, on the final judgement of a typing derivation, of inserting
uses of the intersection-introduction typing rule at some (possibly
deeply nested) positions, without actually needing to build the new
derivation.  Recently, we have improved on this technique by
introducing _expansion variables_ (E-variables), which make the
calculation straightforward and understandable.  E-variables make it
easy to postpone choices of which typing rules to use until later
constraint solving gives enough information to allow making a good
choice.

Expansion can also be done for type constructors other than
intersection, such as the ! of Linear Logic or the familiar forall
quantifier, and E-variables make this easy.

This talk explains the best current knowledge about expansion and
how it can be used.