FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Gradual Intersection Types

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: