{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T05:48:56Z","timestamp":1784180936126,"version":"3.55.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF Career Award Christos Dimoulas","award":["CCF-2237984"],"award-info":[{"award-number":["CCF-2237984"]}]},{"name":"NSF SHF: Semantic Foundations for Gradual Typing","award":["CCF-1910522"],"award-info":[{"award-number":["CCF-1910522"]}]},{"name":"DARPA V-SPELLS: POLYMORPH: Promotion to Optimal Languages Yielding Modular Operator-Driven Replacements and Programmatic Hooks","award":["N66001-21-C-4023"],"award-info":[{"award-number":["N66001-21-C-4023"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>In gradual typing, different languages perform different dynamic type checks for the same program even \nthough the languages have the same static type system. This raises the question of whether, given a gradually \ntyped language, the combination of the translation that injects checks in well-typed terms and the dynamic \nsemantics that determines their behavior sufficiently enforce the static type system of the language. Neither \ntype soundness, nor complete monitoring, nor any other meta-theoretic property of gradually typed languages \nto date provides a satisfying answer.<\/jats:p>\n          <jats:p>In response, we present vigilance, a semantic analytical instrument that defines when the check-injecting \ntranslation and dynamic semantics of a gradually typed language are adequate for its static type system. \nTechnically, vigilance asks if a given translation-and-semantics combination enforces the complete run-time \ntyping history of a value, which consists of all of the types associated with the value. We show that the standard \ncombination for so-called Natural gradual typing is vigilant for the standard simple type system, but the \nstandard combination for Transient gradual typing is not. At the same time, the standard combination for \nTransient is vigilant for a tag type system but the standard combination for Natural is not. Hence, we clarify \nthe comparative type-level reasoning power between the two most studied approaches to sound gradual typing. \nFurthermore, as an exercise that demonstrates how vigilance can guide design, we introduce and examine \na new theoretical static gradual type system, dubbed truer, that is stronger than tag typing and more faithfully \nreflects the type-level reasoning power that the dynamic semantics of Transient gradual typing can guarantee.<\/jats:p>","DOI":"10.1145\/3649842","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"864-892","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Gradually Typed Languages Should Be Vigilant!"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-8850-0984","authenticated-orcid":false,"given":"Olek","family":"Gierczak","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-9583-4448","authenticated-orcid":false,"given":"Lucy","family":"Menon","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9338-7034","authenticated-orcid":false,"given":"Christos","family":"Dimoulas","sequence":"additional","affiliation":[{"name":"Northwestern University, Evanston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7424-572X","authenticated-orcid":false,"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_2_2_4_1","unstructured":"Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. USA. https:\/\/dl.acm.org\/doi\/10.5555\/1037736"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434342"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133872"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_11"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276503"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676967"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","unstructured":"Ben Greenman. 2022. Deep and shallow types for gradual languages. In PLDI. 580\u2013593. https:\/\/doi.org\/10.1145\/3519939.3523430 10.1145\/3519939.3523430","DOI":"10.1145\/3519939.3523430"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579833"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3235045"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360548"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000217"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110284"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434288"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314627"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473573"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607836"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498930"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133880"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290328"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000125"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_2_29_1","volume-title":"Higher Order Operational Techniques in Semantics","author":"Pitts Andrew","unstructured":"Andrew Pitts and Ian Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics, Andrew Gordon and Andrew Pitts (Eds.). Publications of the Newton Institute, Cambridge University Press, 227\u2013273. http:\/\/www.inf.ed.ac.uk\/~stark\/operfl.html"},{"key":"e_1_2_2_30_1","volume-title":"Reddy and Hongseok Yang","author":"Uday","year":"2003","unstructured":"Uday S. Reddy and Hongseok Yang. 2003. Correctness of Data Representations Involving Heap Data Structures. In Programming Languages and Systems, Pierpaolo Degano (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 223\u2013237. isbn:978-3-540-36575-4 https:\/\/dl.acm.org\/doi\/10.5555\/1765712.1765730"},{"key":"e_1_2_2_31_1","volume-title":"Proceedings of the 2006 Workshop on Scheme and Functional Programming Workshop. 81\u201392","author":"Jeremy","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Proceedings of the 2006 Workshop on Scheme and Functional Programming Workshop. 81\u201392. http:\/\/scheme2006.cs.uchicago.edu\/13-siek.pdf"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359619.3359742"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009849"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649842","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649842","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649842"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":39,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649842"],"URL":"https:\/\/doi.org\/10.1145\/3649842","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}