To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 25/05/09 - 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 25 mai, 10h30

                          ------------------------
                          Francesco Zappa Nardelli
                          ------------------------

                                   INRIA

                                 ==========
                                 Like types
                                 ==========

Many large software systems originate from untyped scripting language
code.  While good for initial development, this can impact
code-quality and performance in the long run.  We present an approach
for integrating untyped and typed code in the same system in order to
allow an initial script to be smoothly evolved into a more efficient
and robust system.  Our approach adds a novel intermediate point,
called "like types", between dynamic and static types. Uses of
variables of like type are checked statically, while conformance of a
value to a like type is checked at run-time individually at each
access.

We show that, in contrast to previous proposals, this approach
captures common programmer mistakes, is compatible with
object-orientation and can be implemented efficiently.  The parts of a
program annotated with concrete types enjoy the usual static safety
guarantees and can be optimised, while like types improve local safety
and integrate smoothly with untyped parts of a program without
hindering performance. We prove the soundness of our design, describe
our implementation in the Thorn language, and evaluate our design and
implementation by adding type information to pre-existing untyped
code.

Collaboration avec T. Wrigstad, S. Lebresne, J. Östlund, J. Vitek
(Purdue University).