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

The polymorphic blame calculus integrates static typing, including
universal types, with dynamic typing. The primary challenge with this
integration is preserving parametricity: even dynamically-typed code
should satisfy it once it has been cast to a universal type. Ahmed et
al. (2011) employ runtime type generation in the polymorphic blame
calculus to preserve parametricity, but a proof that it does so has
been elusive. Matthews and Ahmed (2008) gave a proof of parametricity
for a closely related system that combines ML and Scheme, but later
found a flaw in their proof. In this paper we present an improved
version of the polymorphic blame calculus and we prove that it
satisfies relational parametricity. The proof relies on a step-indexed
Kripke logical relation. The step-indexing is required to make the
logical relation well-defined in the case for the dynamic type. The
possible worlds include the mapping of generated type names to their
types and the mapping of type names to relations. We prove the
Fundamental Property of this logical relation and that it is sound
with respect to contextual equivalence. To demonstrate the utility of
parametricity in the polymorphic blame calculus, we derive two free

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

15:00 - 16:10
Integrating Static and Dynamic TypingResearch Papers at L1
Chair(s): Ronald GarciaUniversity of British Columbia
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
On Polymorphic Gradual Typing
Research Papers
Yuu IgarashiKyoto University, Japan, Taro SekiyamaIBM Research, Japan, Atsushi IgarashiKyoto University, Japan
Gradual Typing with Union and Intersection Types
Research Papers
Giuseppe CastagnaCNRS, France / University of Paris Diderot, France, Victor LanvinENS Cachan, France