Paper Info
Title
CPS transformation with affine types for call-by-value implicit polymorphism
Abstract
AbstractTransformation of programs into continuation-passing style (CPS) reveals the notion of continuations, enabling many applications such as control operators and intermediate representations in compilers. Although type preservation makes CPS transformation more beneficial, achieving type-preserving CPS transformation for implicit polymorphism with call-by-value (CBV) semantics is known to be challenging. We identify the difficulty in the problem that we call scope intrusion. To address this problem, we propose a new CPS target language Λopen that supports two additional constructs for polymorphism: one only binds and the other only generalizes type variables. Unfortunately, their unrestricted use makes Λopen unsafe due to undesired generalization of type variables. We thus equip Λopen with affine types to allow only the type-safe generalization. We then define a CPS transformation from Curry-style CBV System F to type-safe Λopen and prove that the transformation is meaning and type preserving. We also study parametricity of Λopen as it is a fundamental property of polymorphic languages and plays a key role in applications of CPS transformation. To establish parametricity, we construct a parametric, step-indexed Kripke logical relation for Λopen and prove that it satisfies the Fundamental Property as well as soundness with respect to contextual equivalence.
Year
DOI
Venue
2021
10.1145/3473600
Proceedings of the ACM on Programming Languages
Keywords
DocType
Volume
continuation-passing style, polymorphism, affine types, parametricity
Journal
5
Issue
Citations 
PageRank 
ICFP
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
Taro Sekiyama1195.76
Takeshi Tsukada202.03