Séminaire Cambium, Inria Paris
                                     BJ09
                           Vendredi 27 mars, 10h30

                                  Litao Zhou

         An Elaboration-Based Foundation for OCaml Recursive Modules

OCaml recursive modules are a powerful but complex feature. While useful for
modular programming, they suffer from the so-called double vision problem, which
occurs when the type system fails to recognize that some external abstract type
and its internal concrete definition are indeed the same, which leads to
undesired typechecking failures. Although OCaml features both generative and
applicative functors, recursive modules have historically been formally studied
with a focus on generative functors.

In this talk, I will present a formal foundation for recursive modules with both
generative and applicative functors in the language M-omega-mu, an extension of
Blaudeau's M-omega formalization of OCaml modules with recursive modules. Typing
is defined by elaboration into System F-omega-mu, an extension of F-omega with
equi-recursive types.

We start in the absence of double vision by elaborating recursive modules as
fixpoints of functors, mapping from external signatures to module bodies. To
cope with recursive applicative functors, we will extend the F-omega-mu library
of transparent existentials with two new primitives. This enables a uniform
treatment for all functor types. The double vision problem will be addressed
following Dreyer's approach, but elaboration suggests that it can actually be
understood as a source-level encoding into recursive modules without double
vision.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.