{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:14:36Z","timestamp":1754486076709,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-21-1-0054"],"award-info":[{"award-number":["FA9550-21-1-0054"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004040","name":"KU Leuven","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004040","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":[[2021,1,4]]},"abstract":"<jats:p>What is a good gradual language? Siek et al. have previously proposed the refined criteria, a set of formal ideas that characterize a range of guarantees typically expected from a gradual language. While these go a long way, they are mostly focused on syntactic and type safety properties and fail to characterize how richer semantic properties and reasoning principles that hold in the static language, like non-interference or parametricity for instance, should be upheld in the gradualization.<\/jats:p>\n          <jats:p>\n            In this paper, we investigate and argue for a new criterion previously hinted at by Devriese et al.: the embedding from the static to the gradual language should be fully abstract. Rather than preserving an arbitrarily chosen interpretation of source language types, this criterion requires that\n            <jats:italic>all<\/jats:italic>\n            source language equivalences are preserved. We demonstrate that the criterion weeds out erroneous gradualizations that nevertheless satisfy the refined criteria. At the same time, we demonstrate that the criterion is realistic by reporting on a mechanized proof that the property holds for a standard example: GTLC\n            <jats:sub>\u00b5<\/jats:sub>\n            , the natural gradualization of STLC\n            <jats:sub>\u00b5<\/jats:sub>\n            , the simply typed lambda-calculus with equirecursive types. We argue thus that the criterion is useful for understanding, evaluating, and guiding the design of gradual languages, particularly those which are intended to preserve source language guarantees in a rich way.\n          <\/jats:p>","DOI":"10.1145\/3434288","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Fully abstract from static to gradual"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1645-6876","authenticated-orcid":false,"given":"Koen","family":"Jacobs","sequence":"first","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3862-6856","authenticated-orcid":false,"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Brussel, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49255-0_70"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055109"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00025"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_2_1_6_1","unstructured":"Amal Ahmed Lindsey Kuper and Jacob Matthews. 2011b. Parametric polymorphism through run-time sealing or Theorems for low low prices ! http:\/\/www.ccs.neu.edu\/home\/amal\/papers\/paramseal-tr.pdf  Amal Ahmed Lindsey Kuper and Jacob Matthews. 2011b. Parametric polymorphism through run-time sealing or Theorems for low low prices ! http:\/\/www.ccs.neu.edu\/home\/amal\/papers\/paramseal-tr.pdf"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628149"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837618"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158126"},{"key":"e_1_2_1_11_1","unstructured":"Dominique Devriese Marco Patrignani and Frank Piessens. 2020. Two Parametricities versus Three Universal Types. ( 2020 ). http:\/\/soft.vub.ac.be\/~dodevrie\/poly-seal-no-j-201910.pdf Submitted to the Journal of the ACM.  Dominique Devriese Marco Patrignani and Frank Piessens. 2020. Two Parametricities versus Three Universal Types. ( 2020 ). http:\/\/soft.vub.ac.be\/~dodevrie\/poly-seal-no-j-201910.pdf Submitted to the Journal of the ACM."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:2)2017"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837670"},{"key":"e_1_2_1_16_1","unstructured":"Ronald Garcia and \u00c9ric Tanter. 2015. Deriving a Simple Gradual Security Language. arXiv preprint arXiv:1511.01399 ( 2015 ).  Ronald Garcia and \u00c9ric Tanter. 2015. Deriving a Simple Gradual Security Language. arXiv preprint arXiv:1511.01399 ( 2015 )."},{"volume-title":"Workshop on Gradual Typing.","author":"Ronald","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2019.6"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360548"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000169"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","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 ).  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 ).","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_2"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022670.2951941"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.011"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699503"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_2_1_29_1","first-page":"513","article-title":"Types, Abstraction, and Parametric Polymorphism. In Information Processing","author":"Reynolds J. C.","year":"1983","journal-title":"North Holland"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_29"},{"key":"e_1_2_1_31_1","unstructured":"Jeremy Siek. 2019. GitHub-jsiek\/gradual-typing-in-agda: Formalizations of Gradually Typed Languages in Agda. https: \/\/github.com\/jsiek\/gradual-typing-in-agda. (Accessed on 10\/18\/ 2019 ).  Jeremy Siek. 2019. GitHub-jsiek\/gradual-typing-in-agda: Formalizations of Gradually Typed Languages in Agda. https: \/\/github.com\/jsiek\/gradual-typing-in-agda. (Accessed on 10\/18\/ 2019 )."},{"key":"e_1_2_1_32_1","first-page":"81","volume-title":"Scheme and Functional Programming Workshop","volume":"6","author":"Siek Jeremy G","year":"2006"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341709"},{"volume-title":"CoqPL, Date: 2017 \/01\/21-2017\/01\/21","author":"Timany Amin","key":"e_1_2_1_35_1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328486"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434288","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434288","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434288","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434288"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":41,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434288"],"URL":"https:\/\/doi.org\/10.1145\/3434288","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}