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 25 février, 10h30

                               -------------
                               Hyeonseung Im
                               -------------

                                    LRI

           =====================================================
           Towards a syntactic type system for recursive modules
           =====================================================

A type system for ML-style recursive modules should address at least two
technical challenges. First, it needs to solve the double vision problem,
which refers to an inconsistency between external and internal views of
recursive modules. Second, and more importantly, it needs to handle cyclic
type definitions caused by recursion between modules to typecheck common
patterns of recursive modules including functor fixpoints.

In this talk, I will first present a syntactic type system for recursive
modules without type parameters that solves the double vision problem and
accounts for cyclic type definitions. Then, I will discuss how to extend our
type system with type parameters in a rather simplified setting, but still
allowing us to define abstract types and arbitrary recursive type definitions
with type parameters. In particular, I will discuss unsound interaction
between non-contractive recursive types and abstract types, and present a new
semantic notion of contractiveness for types and signatures.  Our type system
with semantic contractiveness is sound with respect to the standard
call-by-value operational semantics, which eliminates signature
sealings. Another notable result is that while non-contractive types in
signatures lead to unsoundness of the type system, they may be allowed in
modules. I hopefully expect that we can extend our results to a full-fledged
module system à la OCaml.