[Pl-seminar] 6/23 Seminar: Dustin Jamner, Relational Parametricity for Polymorphic Blame Calculus

[Daniel Patterson]

NUPRL Seminar presents

Dustin Jamner
Northeastern University

12:00
Friday, June 23 2017
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Relational Parametricity for Polymorphic Blame Calculus

Abstract:

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 work we prove that the polymorphic blame
calculus 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
concrete 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.


Bio:

Dustin Jamner is an undergraduate at Northeastern University in Computer
Science, working with Amal Ahmed.