Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                                    Online
                          Vendredi 1 décembre, 10h30

                              Sergei Stepanenko
                              Aarhus University

               The Essence of Generalized Algebraic Data Types

Since their introduction twenty years ago, generalized algebraic data
types, commonly referred to as GADTs, have become a staple of modern
functional programming languages. First introduced as an extension of
the Glasgow Haskell Compiler, they were since adopted by OCaml, Scala
and many other programming languages, due to their ability to
establish more precise specifications for algebraic type constructors.
These implementations, and the associated difficulties, have also
resulted in a rich literature that tackles the problems of type
inference in languages with ML-style polymorphism and GADTs. However,
one feature that remains understudied is the semantics of GADTs and
the nature and expressivity of these types.

In this presentation, we demonstrate an extension of System Fω with
recursive types and internalized type equalities with injective type
constructors. Using this calculus, we can express GADTs encountered in
the wild. Finally, we build two relational models of our calculus: a
simple, unary model that illustrates a novel, two-stage interpretation
technique, necessary to account for the equational constraints; and a
more sophisticated, binary model that relaxes the construction to
allow, for the first time, formal reasoning about data-abstraction in
a calculus equipped with GADTs.

            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.