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 - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 1, bâtiment C Lundi 18 février, 10h30 ------------- Victor Lanvin ------------- IRIF ================================= Gradual Typing: A New Perspective ================================= Gradual typing is a recent approach that aims at embedding both static typing and dynamic typing inside the same language. This allows the programmer to get the best of both worlds, by finely tuning the distribution of dynamic and static type checking over a program. However, this "gradualization" is sometimes too coarse, and an expression is often either fully dynamic or fully static. We argue that we can solve this issue by combining gradual typing with union and intersection types, and further extend this framework to a polymorphic setting. Unfortunately, this kind of type discipline is out of reach of current gradual type systems. Gradual type systems are often defined using syntactic notions on types, which make them difficult to extend with more semantic notions such as union and intersection types. To solve this problem, we explore a new, more semantic way to interpret gradual types, and use this new approach to define three gradual types systems: (i) Hindley-Milner, (ii) with subtyping, and (iii) with set-theoretic types. These new systems are defined both declaratively -- by simply adding two subsumption rules -- and algorithmically -- by reusing existing techniques on non-gradual types.