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
theorems.

Wed 6 Sep

Displayed time zone: Belfast change

15:00 - 16:10
Integrating Static and Dynamic TypingResearch Papers at L1
Chair(s): Ronald Garcia University of British Columbia
15:00
23m
Talk
Theorems for Free for Free: Parametricity, With and Without Types
Research Papers
Amal Ahmed Northeastern University, USA, Dustin Jamner Northeastern University, USA, Jeremy G. Siek Indiana University, USA, Philip Wadler University of Edinburgh, UK
DOI
15:23
23m
Talk
On Polymorphic Gradual Typing
Research Papers
Yuu Igarashi Kyoto University, Japan, Taro Sekiyama IBM Research, Japan, Atsushi Igarashi Kyoto University, Japan
DOI
15:46
23m
Talk
Gradual Typing with Union and Intersection Types
Research Papers
Giuseppe Castagna CNRS, France / University of Paris Diderot, France, Victor Lanvin ENS Cachan, France
DOI