Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Wed 6 Sep 2017 15:46 - 16:10 at L1 - Integrating Static and Dynamic Typing Chair(s): Ronald Garcia

We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to gradual ones and likewise for the subtyping relation. We also show that deciding subtyping for gradual types can be reduced in linear time to deciding subtyping on non-gradual types and that the same holds true for all subtyping-related decision problems that must be solved for type inference. More generally, this work not only enriches gradual type systems with unions and intersections and with the type precision that arise from their use, but also proposes and advocates a new style of gradual types programming where union and intersection types are used by programmers to instruct the system to perform fewer dynamic checks.

Wed 6 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast change

15:00 - 16:10
Integrating Static and Dynamic TypingResearch Papers at L1
Chair(s): Ronald GarciaUniversity of British Columbia
15:00
23m
Talk
Theorems for Free for Free: Parametricity, With and Without Types
Research Papers
Amal AhmedNortheastern University, USA, Dustin JamnerNortheastern University, USA, Jeremy G. SiekIndiana University, USA, Philip WadlerUniversity of Edinburgh, UK
DOI
15:23
23m
Talk
On Polymorphic Gradual Typing
Research Papers
Yuu IgarashiKyoto University, Japan, Taro SekiyamaIBM Research, Japan, Atsushi IgarashiKyoto University, Japan
DOI
15:46
23m
Talk
Gradual Typing with Union and Intersection Types
Research Papers
Giuseppe CastagnaCNRS, France / University of Paris Diderot, France, Victor LanvinENS Cachan, France
DOI