{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:21:03Z","timestamp":1750220463256,"version":"3.41.0"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"JST ERATO","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}]},{"name":"JSPS KAKENHI","award":["JP19K20247, JP19K20211"],"award-info":[{"award-number":["JP19K20247, JP19K20211"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,8,22]]},"abstract":"<jats:p>\n            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 \u039b\n            <jats:sup>\n              <jats:italic>open<\/jats:italic>\n            <\/jats:sup>\n            that supports two additional constructs for polymorphism: one only binds and the other only generalizes type variables. Unfortunately, their unrestricted use makes \u039b\n            <jats:sup>\n              <jats:italic>open<\/jats:italic>\n            <\/jats:sup>\n            unsafe due to undesired generalization of type variables. We thus equip \u039b\n            <jats:sup>\n              <jats:italic>open<\/jats:italic>\n            <\/jats:sup>\n            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 \u039b\n            <jats:sup>\n              <jats:italic>open<\/jats:italic>\n            <\/jats:sup>\n            and prove that the transformation is meaning and type preserving. We also study parametricity of \u039b\n            <jats:sup>\n              <jats:italic>open<\/jats:italic>\n            <\/jats:sup>\n            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 \u039b\n            <jats:sup>\n              <jats:italic>open<\/jats:italic>\n            <\/jats:sup>\n            and prove that it satisfies the Fundamental Property as well as soundness with respect to contextual equivalence.\n          <\/jats:p>","DOI":"10.1145\/3473600","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["CPS transformation with affine types for call-by-value implicit polymorphism"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[{"name":"Chiba University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034830"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"volume-title":"Compiling with Continuations","author":"Appel Andrew W.","key":"e_1_2_2_5_1"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54444-5_83"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"volume-title":"Plotkin","year":"1996","author":"Barber Andrew","key":"e_1_2_2_9_1"},{"volume-title":"Proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW\u201901)","year":"2001","author":"Berdine Josh","key":"e_1_2_2_10_1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020891112409"},{"key":"e_1_2_2_12_1","unstructured":"Joshua James Berdine. 2004. Linear and Affine Typing of Continuation-Passing Style. RR-04-04.  Joshua James Berdine. 2004. Linear and Affine Typing of Continuation-Passing Style. RR-04-04."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2794078"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158110"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561339"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341643"},{"key":"e_1_2_2_17_1","unstructured":"Olivier Danvy. 1992. Three Steps for the CPS Transformation. CIS-92-2.  Olivier Danvy. 1992. Three Steps for the CPS Transformation. CIS-92-2."},{"key":"e_1_2_2_18_1","unstructured":"Olivier Danvy and Andrzej Filinski. 1989. A functional abstraction of typed contexts.  Olivier Danvy and Andrzej Filinski. 1989. A functional abstraction of typed contexts."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"volume-title":"Actes WSA\u201992 Workshop on Static Analysis","year":"1992","author":"Danvy Olivier","key":"e_1_2_2_20_1"},{"volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS \u201986)","author":"Felleisen Matthias","key":"e_1_2_2_21_1"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/800235.807077"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507639"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318654"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24754-8_15"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_29_1","unstructured":"J. Y. Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Universit\u00e9 Paris 7.  J. Y. Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Universit\u00e9 Paris 7."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4"},{"key":"e_1_2_2_31_1","unstructured":"Robert Harper and Mark Lillibridge. 1991. ML with callcc is unsound. Announcement on the types electronic forum. https:\/\/www.cis.upenn.edu\/~bcpierce\/types\/archives\/1991\/msg00034.html  Robert Harper and Mark Lillibridge. 1991. ML with callcc is unsound. Announcement on the types electronic forum. https:\/\/www.cis.upenn.edu\/~bcpierce\/types\/archives\/1991\/msg00034.html"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158630"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019463"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45788-7_10"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.18"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287604"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032742"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78969-7_18"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000320"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291179"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487246"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2015.7054200"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567077"},{"key":"e_1_2_2_44_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2020. The OCaml system release 4.10: Documentation and user\u2019s manua. https:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/  Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2020. The OCaml system release 4.10: Documentation and user\u2019s manua. https:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99622"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00022-2"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_17"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480926"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000165"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57182-5_8"},{"key":"e_1_2_2_57_1","unstructured":"Gordon D. Plotkin. 1973. Lambda-definability and logical relations.  Gordon D. Plotkin. 1973. Lambda-definability and logical relations."},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"volume-title":"Abstraction and Parametric Polymorphism. In IFIP Congress. 513\u2013523","year":"1983","author":"Reynolds John C.","key":"e_1_2_2_61_1"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019459"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_13"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408999"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604144"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_20"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224168"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_24"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473600","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473600","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:48:14Z","timestamp":1750193294000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473600"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":72,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473600"],"URL":"https:\/\/doi.org\/10.1145\/3473600","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}