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

15:00 - 16:10: Research Papers - Integrating Static and Dynamic Typing at L1
Chair(s): Ronald GarciaUniversity of British Columbia
icfp-2017-papers150470280000015:00 - 15:23
Amal AhmedNortheastern University, USA, Dustin JamnerNortheastern University, USA, Jeremy G. SiekIndiana University, USA, Philip WadlerUniversity of Edinburgh, UK
icfp-2017-papers150470420000015:23 - 15:46
Yuu IgarashiKyoto University, Japan, Taro SekiyamaIBM Research, Japan, Atsushi IgarashiKyoto University, Japan
icfp-2017-papers150470560000015:46 - 16:10
Giuseppe CastagnaCNRS, France / University of Paris Diderot, France, Victor LanvinENS Cachan, France