{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T22:37:05Z","timestamp":1726439825396},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100000038","name":"National Sciences and Engineering Research Council of Canada","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"\n Abstracting Gradual Typing (AGT) is a systematic approach to designing gradually-typed languages. Languages developed using AGT automatically satisfy the formal\n semantic<\/jats:italic>\n criteria for gradual languages identified by Siek et al. Nonetheless, vanilla AGT semantics can still have important shortcomings. First, a gradual language's runtime checks should preserve the\n space-efficiency<\/jats:italic>\n guarantees inherent to the underlying static and dynamic languages. To the contrary, the default operational semantics of AGT break proper tail calls. Second, a gradual language's runtime checks should enforce basic modular type-based invariants expected from the static type discipline. To the contrary, the default operational semantics of AGT may fail to enforce some invariants in surprising ways. We demonstrate this in the GTFL\n \u2272<\/jats:sub>\n language of Garcia et al.\n <\/jats:p>\n \n This paper addresses both problems at once by refining the theory underlying AGT's dynamic checks. Garcia et al. observe that AGT involves\n two<\/jats:italic>\n abstractions of static types: one for the static semantics and one for the dynamic semantics. We recast the latter as an abstract interpretation of\n subtyping<\/jats:italic>\n itself, while gradual types still abstract static types. Then we show how\n forward-completeness<\/jats:italic>\n (Giacobazzi and Quintarelli) is key to supporting both space-efficient execution and reliable runtime type enforcement.\n <\/jats:p>","DOI":"10.1145\/3434342","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-28","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Abstracting gradual typing moving forward: precise and space-efficient"],"prefix":"10.1145","volume":"5","author":[{"given":"Felipe","family":"Ba\u00f1ados Schwerter","sequence":"first","affiliation":[{"name":"University of British Columbia, Canada"}]},{"given":"Alison M.","family":"Clark","sequence":"additional","affiliation":[{"name":"n.n., n.n."}]},{"given":"Khurram A.","family":"Jafery","sequence":"additional","affiliation":[{"name":"Amazon, Canada"}]},{"given":"Ronald","family":"Garcia","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4111019"},{"volume-title":"echnical Report). arXiv","year":"2010","author":"Schwerter Felipe Ba\u00f1ados","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628149"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_6_1","unstructured":"Tim Disney and Cormac Flanagan. 2011. Gradual information flow typing. https:\/\/users.soe.ucsc.edu\/~cormac\/papers\/ stop11.pdf Tim Disney and Cormac Flanagan. 2011. Gradual information flow typing. https:\/\/users.soe.ucsc.edu\/~cormac\/papers\/ stop11.pdf"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647170.718288"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048114"},{"volume-title":"Topology","year":"2000","author":"Munkres James R.","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"volume-title":"Types and programming languages","author":"Pierce Benjamin C.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75284"},{"volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi Davide","key":"e_1_2_1_17_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511777110"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_29"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1570506.1570511"},{"key":"e_1_2_1_21_1","first-page":"81","volume-title":"Proc. Scheme and Functional Programming Workshop","author":"Jeremy","year":"2006"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102496"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276945.3276947"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_1_29_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\/pdf\/10.1145\/3434342","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T00:47:18Z","timestamp":1672620438000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434342"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":29,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434342"],"URL":"https:\/\/doi.org\/10.1145\/3434342","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"}}]}}