Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!

by: Jacob Matthews, Amal Ahmed

Programming Languages and Systems (2008), pp. 16-31.

View FullText article

Springer (DOI)

Reviews [Write a review of this article]

There are no reviews of this article

Find related articles from these CiteULike users

msakai, shimomura

Find related articles with these CiteULike tags

2008, polymorphism, systemf, type

Abstract

We show how to extend System F’s parametricity guarantee to a Matthews-Findler-style multi-language system that combines System F with an untyped language by use of dynamic sealing. While the use of sealing for this purpose has been suggested before, it has never been proven to preserve parametricity. In this paper we prove that it does using step-indexed logical relations. Using this result we show a scheme for implementing parametric higher-order contracts in an untyped setting which corresponds to a translation given by Sumii and Pierce. These contracts satisfy rich enough guarantees that we can extract analogues to Wadler’s free theorems that rely on run-time enforcement of dynamic seals.

@incollection{citeulike:2997653, abstract = {We show how to extend System\ F’s parametricity guarantee to a Matthews-Findler-style multi-language system that combines System\ F with an untyped language by use of dynamic sealing. While the use of sealing for this purpose has been suggested before, it has never been proven to preserve parametricity. In this paper we prove that it does using step-indexed logical relations. Using this result we show a scheme for implementing parametric higher-order contracts in an untyped setting which corresponds to a translation given by Sumii and Pierce. These contracts satisfy rich enough guarantees that we can extract analogues to Wadler’s free theorems that rely on run-time enforcement of dynamic seals.}, author = {Matthews, Jacob and Ahmed, Amal }, citeulike-article-id = {2997653}, doi = {10.1007/978-3-540-78739-6\_2}, journal = {Programming Languages and Systems}, keywords = {polymorphism}, pages = {16--31}, posted-at = {2008-07-15 02:35:53}, priority = {2}, title = {Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!}, url = {http://dx.doi.org/10.1007/978-3-540-78739-6\_2}, year = {2008} }

RIS record

TY - CHAP ID - citeulike:2997653 L3 - citeulike-article-id:2997653 TI - Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices! JF - Programming Languages and Systems SP - 16 EP - 31 N2 - We show how to extend System F’s parametricity guarantee to a Matthews-Findler-style multi-language system that combines System F with an untyped language by use of dynamic sealing. While the use of sealing for this purpose has been suggested before, it has never been proven to preserve parametricity. In this paper we prove that it does using step-indexed logical relations. Using this result we show a scheme for implementing parametric higher-order contracts in an untyped setting which corresponds to a translation given by Sumii and Pierce. These contracts satisfy rich enough guarantees that we can extract analogues to Wadler’s free theorems that rely on run-time enforcement of dynamic seals. KW - polymorphism AU - Matthews, Jacob AU - Ahmed, Amal PY - 2008/// UR - http://dx.doi.org/10.1007/978-3-540-78739-6_2 ER -

RIS BibTeX