Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

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

Jacob MatthewsContact Information and Amal AhmedContact Information

(1)  University of Chicago,  
(2)  Toyota Technological Institute at Chicago,  
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.

Contact Information Jacob Matthews
Email: jacobm@cs.uchicago.edu

Contact Information Amal Ahmed
Email: amal@tti-c.org
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.111 • Server: mpweb03
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)