Authors: Pedro Ângelo and Mário Florido
Paper Information
Title: | Gradual Intersection Types |
Authors: | Pedro Ângelo and Mário Florido |
Proceedings: | ITRS Full papers |
Editor: | Michele Pagani |
Keywords: | intersection types, gradual typing, discrete polymorphism, lambda calculus |
Abstract: | ABSTRACT. Gradual typing integrates dynamic and static types. Since its introduction, it has been successfully applied to several extensions of simple types, including subtyping, parametric polymorphism and substructural types. This work studies its application to intersection type systems. We introduce a new approach to define a gradual version of the original intersection type system of Coppo and Dezani. We then present a new operational semantics for terms typed with static and dynamic intersection types, which enables dynamic type casts and identifies the causes for type errors in a framework inspired by the blame calculus. Finally we prove several properties of our system including a correctness criteria and soundness of the extension of the original gradual type system. |
Pages: | 33 |
Talk: | Jul 08 15:00 (Session 40J) |
Paper: |