LunarMLの型付きCPSメモ

@article{10.1145/319301.319345,
author = {Morrisett, Greg and Walker, David and Crary, Karl and Glew, Neal},
title = {From system F to typed assembly language},
year = {1999},
issue_date = {May 1999},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {21},
number = {3},
issn = {0164-0925},
url = {https://doi.org/10.1145/319301.319345},
doi = {10.1145/319301.319345},
abstract = {We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic   closure conversion that is considerably simpler than previous work. The compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.},
journal = {ACM Trans. Program. Lang. Syst.},
month = may,
pages = {527–568},
numpages = {42},
keywords = {certified code, closure conversion, secure extensible systems, type-directed compilation, typed assembly language, typed intermediate languages}
}

@inproceedings{10.1145/158511.158630,
author = {Harper, Robert and Lillibridge, Mark},
title = {Explicit polymorphism and CPS conversion},
year = {1993},
isbn = {0897915607},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/158511.158630},
doi = {10.1145/158511.158630},
abstract = {We study the typing properties of CPS conversion for an extension of Fω with control operators. Two classes of evaluation strategies are considered, each with call-by-name and call-by-value variants. Under the “standard” strategies, constructor abstractions are values, and constructor applications can lead to non-trivial control effects. In contrast, the “ML-like” strategies evaluate beneath constructor abstractions, reflecting the usual interpretation of programs in languages based on implicit polymorphism. Three continuation passing style sub-languages are considered, one on which the standard strategies coincide, one on which the ML-like strategies coincide, and one on which all strategies coincide. Compositional, type-preserving CPS  transformation algorithms are given for the standard strategies, resulting in terms on which all evaluation strategies coincide. This has as a corollary the soundness and termination of well-typed programs under the standard evaluation strategies. A similar result is obtained for the ML-like call-by-name strategy. In contrast, such results are obtained for the call-by-name strategy. In contrast, such results are obtained for the call-by value ML-like strategy only for a restricted sub-language in which constructor abstractions are limited to values.},
booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {206–219},
numpages = {14},
location = {Charleston, South Carolina, USA},
series = {POPL '93}
}

@article{10.1145/3473600,
author = {Sekiyama, Taro and Tsukada, Takeshi},
title = {CPS transformation with affine types for call-by-value implicit polymorphism},
year = {2021},
issue_date = {August 2021},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {5},
number = {ICFP},
url = {https://doi.org/10.1145/3473600},
doi = {10.1145/3473600},
abstract = {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.},
journal = {Proc. ACM Program. Lang.},
month = aug,
articleno = {95},
numpages = {30},
keywords = {polymorphism, parametricity, continuation-passing style, affine types}
}