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

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn

			     S É M I N A I R E

                   ______                __    _
                  / ____/___ _____ ___  / /_  (_)_  ______ ___
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 11 octobre, 10h30

                               ----------------
                               Clément Blaudeau
                               ----------------

                                 Inria Paris

                  =========================================
                          OCaml modules made simple:
                  insights, formalizations and improvements
                  =========================================

Modularity is a key tool for building reusable and structured code. While the
OCaml module system is known for being expressive and powerful, specifying its
behavior and formalizing its properties has proven to be hard.

In this talk, I will propose a comprehensive description of a (generative)
subset of the OCaml module system (called the source system), with a focus on
the signature avoidance problem.

By extending the signature syntax with existential types (inspired by Fω), we
describe an alternate system (called canonical), that has a simpler set of
judgments, yet solves the issues of the source description and provides formal
guarantees through elaboration into Fω.

I will then show the links between this canonical system and the current OCaml
source, which will reveal key insights on some otherwise hard-to-grasp
mechanisms (signature avoidance, strengthening, etc.). As a middle point
between the path-based representation of OCaml and the formal description of
Fω, the canonical presentation is a framework which we believe could support
numerous features (applicative functors, transparent ascription, module
aliases, etc.) and could serve as a basis for a redefinition of the module
system of an industry-grade language as OCaml.