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

We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed languages, type safety, blame-subtyping theorem, and the gradual guarantee—the so-called refined criteria, advocated by Siek et al. We develop System F_G, which is a gradually typed extension of System F with the dynamic type and a new type consistency relation, and translation to a new polymorphic blame calculus System F_C, which is based on previous polymorphic blame calculi by Ahmed et al. The design of System F_G and System F_C, geared to the criteria, is influenced by the distinction between static and gradual type variables, first observed by Garcia and Cimini. This distinction is also useful to execute statically typed code without incurring additional overhead to manage type names as in the prior calculi. We prove that System F_G satisfies most of the criteria: all but the hardest property of the gradual guarantee on semantics. We show that a key conjecture to prove the gradual guarantee leads to the Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.

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 - 15:23
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 - 15:46
Talk
On Polymorphic Gradual Typing
Research Papers
Yuu IgarashiKyoto University, Japan, Taro SekiyamaIBM Research, Japan, Atsushi IgarashiKyoto University, Japan
DOI
15:46 - 16:10
Talk
Gradual Typing with Union and Intersection Types
Research Papers
Giuseppe CastagnaCNRS, France / University of Paris Diderot, France, Victor LanvinENS Cachan, France
DOI