{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:10:10Z","timestamp":1751663410097,"version":"3.41.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP20H00582, JP19K20247, JP22K17875"],"award-info":[{"award-number":["JP20H00582, JP19K20247, JP22K17875"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"\n Since the arrival of gradual typing, which allows partially typed code in a single program, efficient implementations of gradual typing have been an active research topic. In this paper, we study the space-efficient problem of gradual typing in the presence of parametric polymorphism. Based on the existing work that showed the impossibility of a space-efficient implementation that supports fully parametric polymorphism, this paper will show that a space-efficient implementation is, in principle, possible by slightly relaxing parametricity. We first develop\n \n \n \n \n \n \u03bbC<\/mml:mtext>\n <\/mml:mrow>\n \n m<\/mml:mi>\n p<\/mml:mi>\n <\/mml:mrow>\n \u2200<\/mml:mo>\n <\/mml:msubsup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n , which is a coercion calculus with mostly parametric polymorphism, and show its relaxed parametricity. Then, we present\n \n \n \n \n \n \u03bbS<\/mml:mtext>\n <\/mml:mrow>\n \n m<\/mml:mi>\n p<\/mml:mi>\n <\/mml:mrow>\n \u2200<\/mml:mo>\n <\/mml:msubsup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n , a space-efficient version of\n \n \n \n \n \n \u03bbC<\/mml:mtext>\n <\/mml:mrow>\n \n m<\/mml:mi>\n p<\/mml:mi>\n <\/mml:mrow>\n \u2200<\/mml:mo>\n <\/mml:msubsup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n , and prove that\n \n \n \n \n \n \u03bbS<\/mml:mtext>\n <\/mml:mrow>\n \n m<\/mml:mi>\n p<\/mml:mi>\n <\/mml:mrow>\n \u2200<\/mml:mo>\n <\/mml:msubsup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n programs can be executed in a space-efficient manner and that translation from\n \n \n \n \n \n \u03bbC<\/mml:mtext>\n <\/mml:mrow>\n \n m<\/mml:mi>\n p<\/mml:mi>\n <\/mml:mrow>\n \u2200<\/mml:mo>\n <\/mml:msubsup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n to\n \n \n \n \n \n \u03bbS<\/mml:mtext>\n <\/mml:mrow>\n \n m<\/mml:mi>\n p<\/mml:mi>\n <\/mml:mrow>\n \u2200<\/mml:mo>\n <\/mml:msubsup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n is type-and semantics-preserving.\n <\/jats:p>","DOI":"10.1145\/3656441","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1585-1608","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Space-Efficient Polymorphic Gradual Typing, Mostly Parametric"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5143-9764","authenticated-orcid":false,"given":"Atsushi","family":"Igarashi","sequence":"first","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1772-0580","authenticated-orcid":false,"given":"Shota","family":"Ozaki","sequence":"additional","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"},{"name":"SOKENDAI, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7990-0989","authenticated-orcid":false,"given":"Yudai","family":"Tanabe","sequence":"additional","affiliation":[{"name":"Tokyo Institute of Technology, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000126X"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434342"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133878"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_11"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_4"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103699"},{"key":"e_1_3_2_11_1","unstructured":"Facebook. 2021. Hack. http:\/\/hacklang.org"},{"key":"e_1_3_2_12_1","author":"Flatt Matthew","year":"2010","unstructured":"Matthew Flatt and PLT. 2010. Reference: Racket. Technical Report PLT-TR-2010-1. PLT Design Inc. https:\/\/racket-lang.org\/tr1\/.","journal-title":"Reference: Racket"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_3_2_15_1","first-page":"1","article-title":"Space-efficient Gradual Typing","author":"Herman David","year":"2007","unstructured":"David Herman, Aaron Tomb, and Cormac Flanagan. 2007. Space-efficient Gradual Typing. In Proceedings of the Eighth Symposium on Trends in Functional Programming, TFP 2007, New York City, New York, USA, April 2-4. 2007 (Trends in Functional Programming, Vol. 8), Marco T. Moraz\u00e1n (Ed.). Intellect, 1\u201318.","journal-title":"Proceedings of the Eighth Symposium on Trends in Functional Programming, TFP 2007, New York City, New York, USA, April 2-4. 2007 (Trends in Functional Programming, Vol. 8)"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2020.26"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110284"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314627"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.1.105"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_2"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800529"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290331"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/361932.361937"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133880"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_3_2_28_1","article-title":"Is Space-efficient Polymorphic Gradual Typing Possible?","author":"Ozaki Shota","year":"2021","unstructured":"Shota Ozaki, Taro Sekiyama, and Atsushi Igarashi. 2021. Is Space-efficient Polymorphic Gradual Typing Possible?. In Scheme and Functional Programming Workshop.","journal-title":"Scheme and Functional Programming Workshop"},{"key":"e_1_3_2_29_1","unstructured":"Benjamin Pierce and Eijiro Sumii. 2000. Relating Cryptography and Polymorphism. Manuscript. http:\/\/www.kb.ecei.tohoku.ac.jp\/~sumii\/pub\/infohide.pdf."},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676971"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_4"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1184\/R1\/6608582.v1"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133879"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.17"},{"key":"e_1_3_2_35_1","first-page":"81","article-title":"Gradual Typing for Functional Languages","author":"Siek Jeremy G","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In In Scheme and Functional Programming Workshop. 81\u201392.","journal-title":"In Scheme and Functional Programming Workshop"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737968"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000101"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596598"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837630"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.8"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656441","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656441","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:41:20Z","timestamp":1751661680000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656441"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":48,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656441"],"URL":"https:\/\/doi.org\/10.1145\/3656441","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}