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.