{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,28]],"date-time":"2026-08-28T17:23:39Z","timestamp":1787937819750,"version":"build-2784847793"},"reference-count":29,"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\/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":"<jats:p>\n                    Abstracting Gradual Typing (AGT) is a systematic approach to designing gradually-typed languages. Languages developed using AGT automatically satisfy the formal\n                    <jats:italic toggle=\"yes\">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                    <jats:italic toggle=\"yes\">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                    <jats:sub>\u2272<\/jats:sub>\n                    language of Garcia et al.\n                  <\/jats:p>\n                  <jats:p>\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                    <jats:italic toggle=\"yes\">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                    <jats:italic toggle=\"yes\">subtyping<\/jats:italic>\n                    itself, while gradual types still abstract static types. Then we show how\n                    <jats:italic toggle=\"yes\">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-04T12:34:24Z","timestamp":1609763664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alison M.","family":"Clark","sequence":"additional","affiliation":[{"name":"n.n., n.n."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Khurram A.","family":"Jafery","sequence":"additional","affiliation":[{"name":"Amazon, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ronald","family":"Garcia","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"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"},{"key":"e_1_2_1_3_1","volume-title":"echnical Report). arXiv","author":"Schwerter Felipe Ba\u00f1ados","year":"2010","unstructured":"Felipe Ba\u00f1ados Schwerter, Alison M. Clark, Khurram A. Jafery, and Ronald Garcia. 2020. Abstracting Gradual Typing Moving Forward: Precise and Space-Eficient (Technical Report). arXiv: 2010. 14094 [cs.PL]"},{"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"},{"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"},{"key":"e_1_2_1_13_1","volume-title":"Topology","author":"Munkres James R.","year":"2000","unstructured":"James R. Munkres. 2000. Topology: Second Edition. Prentice Hall, Upper Saddle River, NJ."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_2_1_15_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce. 2002. Types and programming languages. MIT Press, Cambridge, MA, USA."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75284"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","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","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Proc. Scheme and Functional Programming Workshop. University of Chicago Technical Report, Chicago, IL, USA, 81-92. http:\/\/scheme2006.cs.uchicago.edu\/ scheme2006.pdf"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL"},{"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"},{"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"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434342","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434342","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:28:57Z","timestamp":1781854137000},"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":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}