Projects per year
Abstract / Description of output
The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamicallytyped 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 prove that the polymorphic blame calculus satisfies relational parametricity. The proof relies on a stepindexed Kripke logical relation. The stepindexing is required to make the logical relation welldefined 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. To demonstrate the utility of parametricity in the polymorphic blame calculus, we derive two free theorems.
Original language  English 

Article number  39 
Number of pages  28 
Journal  Proceedings of the ACM on Programming Languages 
Volume  1 
Issue number  ICFP 
Early online date  29 Aug 2017 
DOIs  
Publication status  Published  1 Sept 2017 
Fingerprint
Dive into the research topics of 'Theorems for Free for Free: Parametricity, With and Without Types'. Together they form a unique fingerprint.Projects
 1 Finished

From Data Types to Session Types  A Basis for Concurrency and Distribution
20/05/13 → 19/11/20
Project: Research
Profiles

Philip Wadler, FRS
 School of Informatics  Chair of Theoretical Computer Science
 Laboratory for Foundations of Computer Science
 Foundations of Computation
Person: Academic: Research Active