一句话：提出带仿射类型的新 CPS 目标语言 Λ_open，解决 CBV 隐式多态 CPS 变换的类型保持难题并证明参数性。
把程序变换为 CPS 可显式化续元，但按值调用（CBV）隐式多态下保持类型很困难。作者将障碍称为作用域入侵（scope intrusion），并为此提出新的 CPS 目标语言 Λ_open，其中加入两个多态构造：一个只绑定类型变量，另一个只泛化类型变量。由于无限制使用会导致不希望的泛化而不安全，Λ_open 引入仿射类型，只允许类型安全的泛化。作者从 Curry 风格 CBV System F 定义到类型安全 Λ_open 的 CPS 变换，并证明该变换保持意义与类型。论文还研究 Λ_open 的参数性，构造带步指标的 Kripke 逻辑关系，证明其满足 Fundamental Property，并相对于上下文等价是可靠的。
Transformation 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.
@article{paperbot1118,
title = {CPS transformation with affine types for call-by-value implicit polymorphism},
author = {Taro Sekiyama and Takeshi Tsukada},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473600}
}