{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:28:12Z","timestamp":1755217692258,"version":"3.43.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>Gradual typing has long been advocated as a means to bridge the gap between static and dynamic typing disciplines, enabling a range of use cases such as the gradual migration of existing dynamically typed code to more statically typed code, as well as making advanced static typing disciplines more accessible. To assess whether a given gradual language can effectively support these use cases, several formal properties have been proposed, most notably the refined criteria set forth by Siek et al. One criterion asserts that the dynamic extreme of the spectrum should be expressible in the gradual language, formalized by the existence of an adequate embedding from the corresponding dynamic language.<\/jats:p>\n          <jats:p>\n            We observe that the existing dynamic embedding criterion does not capture the desirable property of being able to ascribe embedded code to a static type that it semantically satisfies, and ensure reliable interactions with other components within the gradual language. Specifically, we introduce the notion of\n            <jats:italic toggle=\"yes\">robustness<\/jats:italic>\n            for gradual terms, meaning that when interacting with any gradual context, runtime failures that may occur ought to be caused by the context, not by the robust term itself. We then formulate the\n            <jats:italic toggle=\"yes\">robust dynamic embedding<\/jats:italic>\n            criterion: if a dynamic component semantically satisfies a given static type, then its embedding subsequently ascribed to that static type should be a robust term. We demonstrate that robust dynamic embedding is not implied by any existing metatheoretical property from the literature, and is not upheld by various existing gradual languages. We show that robust dynamic embedding is achievable with a gradualized simply-typed language. All the results are formalized in the Rocq proof assistant. This novel criterion complements the set of criteria for gradual languages and opens several venues for further exploration, in particular for typing disciplines that enforce rich semantic properties.\n          <\/jats:p>","DOI":"10.1145\/3747507","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"66-92","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Robust Dynamic Embedding for Gradual Typing"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1645-6876","authenticated-orcid":false,"given":"Koen","family":"Jacobs","sequence":"first","affiliation":[{"name":"Inria, Nantes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5315-0198","authenticated-orcid":false,"given":"Mat\u00edas","family":"Toro","sequence":"additional","affiliation":[{"name":"University of Chile, Santiago, Chile"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Santiago, Chile"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00025"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 38th Computer Security Foundations Symposium (CSF).","author":"Arquez Dami\u00e1n","year":"2025","unstructured":"Dami\u00e1n Arquez, Mat\u00edas Toro, and \u00c9ric Tanter. 2025. Gradual Sensitivity Typing. In Proceedings of the 38th Computer Security Foundations Symposium (CSF)."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00015"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656442"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009863"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394778"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547627"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the ACM on Programming Languages, 3, ICFP","author":"Eremondi Joseph","year":"2019","unstructured":"Joseph Eremondi, \u00c9ric Tanter, and Ronald Garcia. 2019. Approximate Normalization for Gradual Dependent Types. Proceedings of the ACM on Programming Languages, 3, ICFP (2019), Aug., 88:1\u201388:30."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.22"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837670"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649842"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579833"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the ACM on Programming Languages, 1, ICFP","author":"Igarashi Yuu","year":"2017","unstructured":"Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. Proceedings of the ACM on Programming Languages, 1, ICFP (2017), Sept., 40:1\u201340:29."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527326"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434288"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16265382"},{"key":"e_1_2_1_21_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 (2018)."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527314"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the ACM on Programming Languages, 8, ICFP","author":"Malewski Mara","year":"2024","unstructured":"Mara Malewski, Kenji Maillard, Nicolas Tabareau, and \u00c9ric Tanter. 2024. Gradual Indexed Inductive Types. Proceedings of the ACM on Programming Languages, 8, ICFP (2024), Aug., 255:1\u2013255:29."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360598"},{"volume-title":"A Semantic Foundation for Sound Gradual Typing","author":"New Max S.","key":"e_1_2_1_27_1","unstructured":"Max S. New. 2020. A Semantic Foundation for Sound Gradual Typing. Northeastern University. https:\/\/maxsnew.com\/docs\/dissertation.pdf"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000125"},{"volume-title":"Types and programming languages","author":"Pierce Benjamin C.","key":"e_1_2_1_31_1","unstructured":"Benjamin C. Pierce. 2002. Types and programming languages. MIT press."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_1_33_1","volume-title":"Scheme and Functional Programming Workshop. 6, 81\u201392","author":"Siek Jeremy G","year":"2006","unstructured":"Jeremy G Siek and Walid Taha. 2006. Gradual typing for functional languages. In Scheme and Functional Programming Workshop. 6, 81\u201392."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_2_1_35_1","article-title":"A Logical Approach to Type Soundness","volume":"71","author":"Timany Amin","year":"2024","unstructured":"Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2024. A Logical Approach to Type Soundness. J. ACM, 71, 6 (2024).","journal-title":"J. ACM"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3589207"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009849"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"e_1_2_1_41_1","volume-title":"European Symposium on Programming. 1\u201316","author":"Wadler Philip","year":"2009","unstructured":"Philip Wadler and Robert Bruce Findler. 2009. Well-typed programs can\u2019t be blamed. In European Symposium on Programming. 1\u201316."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747507","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:57:52Z","timestamp":1754413072000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747507"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":41,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747507"],"URL":"https:\/\/doi.org\/10.1145\/3747507","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}