{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:09:26Z","timestamp":1784196566399,"version":"3.55.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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3366-2273","authenticated-orcid":false,"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria, Nantes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7359-890X","authenticated-orcid":false,"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile, Santiago, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00025"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_5_2","article-title":"Gradual Sensitivity Typing","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).","journal-title":"Proceedings of the 38th Computer Security Foundations Symposium (CSF)"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00015"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656442"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009863"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394778"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547627"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"e_1_3_2_14_2","first-page":"224","article-title":"Gradual Security Typing with References","author":"Fennell Luminous","year":"2013","unstructured":"Luminous Fennell and Peter Thiemann. 2013. Gradual Security Typing with References. In Proceedings of the 26th Computer Security Foundations Symposium (CSF). 224\u2013239.","journal-title":"Proceedings of the 26th Computer Security Foundations Symposium (CSF)"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837670"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649842"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3579833"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110284"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527326"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434288"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Koen Jacobs Mat\u00edas Toro Nicolas Tabareau and \u00c9ric Tanter. 2025. Rocq Artifact: Robust Dynamic Embedding for Gradual Typing. doi:10.5281\/zenodo.16265382","DOI":"10.5281\/zenodo.16265382"},{"key":"e_1_3_2_22_2","first-page":"28","article-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic","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).","journal-title":"Journal of Functional Programming"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527314"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674644"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360598"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28263083"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000125"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_2_34_2","first-page":"81","article-title":"Gradual typing for functional languages","volume":"6","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, Vol. 6. 81\u201392.","journal-title":"Scheme and Functional Programming Workshop"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3589207"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009849"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"e_1_3_2_42_2","first-page":"1","volume-title":"European Symposium on Programming","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. Springer, 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":[[2026,7,16]],"date-time":"2026-07-16T10:01:27Z","timestamp":1784196087000},"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":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}