[Pl-seminar] 2/23: Lindsey Kuper, "Parametric polymorphism through run-time sealing, or, theorems for low, low prices!"

[Aaron Turon]

NEU Programming Languages Seminar presents

Lindsey Kuper
Indiana University

Wednesday, 2/23

11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Parametric polymorphism through run-time sealing, or, theorems
for low, low prices!

Abstract: Languages with parametric polymorphism provide the
compile-time guarantee that programs behave uniformly regardless of
the types they are instantiated with.  In such languages, this
parametricity guarantee forms the basis of data abstraction and makes
possible Wadler's "theorems for free!"  In this talk, I'll show how we
can extend System F's parametricity guarantee to a
Matthews-Findler-style multi-language system that combines System F
with a Scheme-like language by use of dynamic sealing, which enforces
data abstraction by using uniquely generated keys to seal values that
should be kept opaque.  While the use of sealing for this purpose has
been suggested before, it has not previously been shown to preserve
parametricity.  Our proof employs a cross-language, step-indexed
logical relation that uses possible worlds to capture the semantics of
seal generation.  Using this possible-worlds model, we can show two
results: first, that System F's parametricity guarantee is preserved
when interoperating with Scheme, and, second, that parametricity is
preserved in a Scheme-only setting that interacts with System F only
to implement a polymorphic contract system.  (This talk describes
current research being done in collaboration with Amal Ahmed and Jacob
Matthews that expands on the work presented in their ESOP 2008 paper
of the same title.)