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

                         VENDREDI 31 janvier, 10h30

                             ------------------
                             Mariangiola Dezani
                             ------------------

                           Università di Torino

              ================================================
              On the Preciseness of Subtyping in Session Types
              ================================================

Subtyping in concurrency has been extensively studied since early 1990s as one
of the most interesting issues in type theory.  The correctness of subtyping
relations has been usually provided as the soundness for type safety.  The
converse direction, the completeness, has been largely ignored in spite of its
usefulness to define the greatest subtyping relation ensuring type safety.
This talk proposes a technique for formalising and proving that a subtyping is
precise (i.e. both sound and complete) with respect to the type safety in
pi-calculus, and applies it to synchronous and asynchronous session calculi.
We first prove that the well-known session subtyping, the branching-selection
subtyping, is sound and complete for the synchronous calculus. Next we show
that in the asynchronous calculus, this subtyping is incomplete for
type-safety: that is, there exist session types T and S such that T can safely
be considered as a subtype of S, but T <= S is not derivable by the
subtyping. We then propose an asynchronous subtyping system which is sound and
complete for the asynchronous calculus.  The method gives a general guidance
to design rigorous channel-based subtypings respecting desired safety
properties.