Flavien Breuvart (Université Paris 13), Graded Types Parametricity : Principles and Application to Abstract Interpretation

Programme

Résumé

In this talk, we will briefly present the yet-to-start project CoGITARe, which aims at developing further graded types expressivity and inference in order to use them to perform abstract interpretations.

In a second time, we give an historic on graded type systems and their expressivity. Then, we will see that this expressivity is limited by a lack of dependency/parametricity. We will thus explore two ongoing research directions that adds two very different kind of parametricity to graded types.

(The provocative title should only be taken as a joke. Despite their apparent similitudes, this work and Éric Tanter's have vastly different objectives and involved different issues and techniques. In particular, notice that gradual and graded types are fundamentally different.)