{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:51:29Z","timestamp":1773809489653,"version":"3.50.1"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>Programmers can use gradual types to migrate programs to have more precise type annotations and thereby improve their readability, efficiency, and safety. Such migration requires an exploration of the migration space and can benefit from tool support, as shown in previous work. Our goal is to provide a foundation for better tool support by settling decidability questions about migration with gradual types. We present three algorithms and a hardness result for deciding key properties and we explain how they can be useful during an exploration. In particular, we show how to decide whether the migration space is finite, whether it has a top element, and whether it is a singleton. We also show that deciding whether it has a maximal element is NP-hard. Our implementation of our algorithms worked as expected on a suite of microbenchmarks.<\/jats:p>","DOI":"10.1145\/3371097","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["What is decidable about gradual types?"],"prefix":"10.1145","volume":"4","author":[{"given":"Zeina","family":"Migeed","sequence":"first","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Understanding TypeScript. In ECOOP 2014 \u2013 Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg","author":"Bierman Gavin","year":"2014"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158103"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290329"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5101"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_2"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Thomas S. Heinze Anders M\u00f8ller and Fabio Strocco. 2016. Type Safety Analysis for Dart. In DLS.  Thomas S. Heinze Anders M\u00f8ller and Fabio Strocco. 2016. Type Safety Analysis for Dart. In DLS.","DOI":"10.1145\/2989225.2989226"},{"key":"e_1_2_2_10_1","volume-title":"Proceedings of POPL, ACM Symposium on Principles of Programming Languages.","author":"Nico"},{"key":"e_1_2_2_11_1","volume-title":"Dynamic Type Inference for Gradual Hindley-Milner Typing. CoRR abs\/1810.12619","author":"Miyazaki Yusuke","year":"2018"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000423"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103714"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2394758.2394762"},{"key":"e_1_2_2_15_1","volume-title":"Siek and Walid Taha","author":"Jeremy","year":"2006"},{"key":"e_1_2_2_16_1","volume-title":"Proceedings of the 2008 Symposium on Dynamic Languages. 7:1\u20137:12","author":"Jeremy"},{"key":"e_1_2_2_17_1","unstructured":"Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015a. Refined Criteria for Gradual Typing. In SNAPL. 274\u2013293.  Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015a. Refined Criteria for Gradual Typing. In SNAPL. 274\u2013293."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775052.2661101"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950343"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371097","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371097","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371097"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":21,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371097"],"URL":"https:\/\/doi.org\/10.1145\/3371097","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}