{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T21:16:36Z","timestamp":1783804596757,"version":"3.55.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["CCF-2102288, CCF-2129344"],"award-info":[{"award-number":["CCF-2102288, CCF-2129344"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>Gradually typed languages allow programmers to mix statically and dynamically typed code, enabling them to incrementally reap the benefits of static typing as they add type annotations to their code. However, this type migration process is typically a manual effort with limited tool support. This paper examines the problem of automated type migration: given a dynamic program, infer additional or improved type annotations. Existing type migration algorithms prioritize different goals, such as maximizing type precision, maintaining compatibility with unmigrated code, and preserving the semantics of the original program. We argue that the type migration problem involves fundamental compromises: optimizing for a single goal often comes at the expense of others. Ideally, a type migration tool would flexibly accommodate a range of user priorities. We present TypeWhich, a new approach to automated type migration for the gradually-typed lambda calculus with some extensions. Unlike prior work, which relies on custom solvers, TypeWhich produces constraints for an off-the-shelf MaxSMT solver. This allows us to easily express objectives, such as minimizing the number of necessary syntactic coercions, and constraining the type of the migration to be compatible with unmigrated code. We present the first comprehensive evaluation of GTLC type migration algorithms, and compare TypeWhich to four other tools from the literature. Our evaluation uses prior benchmarks, and a new set of \"challenge problems.\" Moreover, we design a new evaluation methodology that highlights the subtleties of gradual type migration. In addition, we apply TypeWhich to a suite of benchmarks for Grift, a programming language based on the GTLC. TypeWhich is able to reconstruct all human-written annotations on all but one program.<\/jats:p>","DOI":"10.1145\/3485488","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Solver-based gradual type migration"],"prefix":"10.1145","volume":"5","author":[{"given":"Luna","family":"Phipps-Costin","sequence":"first","affiliation":[{"name":"University of Massachusetts at Amherst, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5717-4210","authenticated-orcid":false,"given":"Carolyn Jane","family":"Anderson","sequence":"additional","affiliation":[{"name":"Wellesley College, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0014-7670","authenticated-orcid":false,"given":"Michael","family":"Greenberg","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arjun","family":"Guha","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Dynamic Inference of Static Types for Ruby. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"An David","year":"2011"},{"key":"e_1_2_2_2_1","volume-title":"Towards Type Inference for JavaScript. In European Conference on Object-Oriented Programming (ECOOP).","author":"Anderson Christopher","year":"2005"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190028"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Nikolaj Bj\u00f8rner Anh-Dung Phan and Lars Fleckenstein. 2015. \u03bd Z: An Optimizing SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS).  Nikolaj Bj\u00f8rner Anh-Dung Phan and Lars Fleckenstein. 2015. \u03bd Z: An Optimizing SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","DOI":"10.1007\/978-3-662-46681-0_14"},{"key":"e_1_2_2_5_1","volume-title":"Extensible Scripting on the JVM. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA).","author":"Bloom Bard","year":"2009"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158103"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236793"},{"key":"e_1_2_2_8_1","volume-title":"Proceedings of the ACM on Programming Languages (PACMPL), 3, POPL","author":"Castagna Giuseppe","year":"2019"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984017"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2518190"},{"key":"e_1_2_2_11_1","volume-title":"Nested Refinements for Dynamic Languages. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"Chugh Ravi","year":"2012"},{"key":"e_1_2_2_12_1","volume-title":"Syntax Errors for LR Parsers. In European Conference on Object-Oriented Programming (ECOOP).","author":"Diekmann Lukas","year":"2020"},{"key":"e_1_2_2_14_1","volume-title":"Catching Bugs in the Web of Program Invariants. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).","author":"Flanagan Cormac","year":"1996"},{"key":"e_1_2_2_15_1","volume-title":"Profile-Guilding Static Typing for Dynamic Scripting Languages. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA).","author":"Furr Michael"},{"key":"e_1_2_2_16_1","volume-title":"Principal Type Schemes for Gradual Programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"Garcia Ronald","year":"2015"},{"key":"e_1_2_2_17_1","unstructured":"Michael Greenberg. 2013. Manifest Contracts. Ph.D. Dissertation. University of Pennsylvania.  Michael Greenberg. 2013. Manifest Contracts. Ph.D. Dissertation. University of Pennsylvania."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236766"},{"key":"e_1_2_2_19_1","volume-title":"On the Cost of Type-Tag Soundness. In ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM).","author":"Greenman Ben","year":"2018"},{"key":"e_1_2_2_20_1","volume-title":"Typing Local Control and State Using Flow Analysis. In European Symposium on Programming (ESOP).","author":"Guha Arjun","year":"2011"},{"key":"e_1_2_2_21_1","volume-title":"Deep Learning Type Inference. In ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE).","author":"Hellendoorn Vincent J.","year":"2018"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224203"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_2_25_1","volume-title":"Heuristic Type Annotation Inference for Ruby. In Dynamic Languages Symposium (DLS).","author":"Kazerounian Milod"},{"key":"e_1_2_2_26_1","volume-title":"ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).","author":"Kuhlenschmidt Andre"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00045"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371097"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290331"},{"key":"e_1_2_2_30_1","volume-title":"Finding Minimum Type Error Sources. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA).","author":"Pavlinovic Zvonimir","year":"2014"},{"key":"e_1_2_2_31_1","volume-title":"Michael Greenberg, and Arjun Guha.","author":"Phipps-Costin Luna","year":"2021"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Michael Pradel Georgios Gousios Jason Liu and Satish Chandra. 2020. TypeWriter: Neural Type Prediction with Search-Based Validation. In Joint Meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE).  Michael Pradel Georgios Gousios Jason Liu and Satish Chandra. 2020. TypeWriter: Neural Type Prediction with Search-Based Validation. In Joint Meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE).","DOI":"10.1145\/3368089.3409715"},{"key":"e_1_2_2_33_1","volume-title":"The Ins and Outs of Gradual Type Inference. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"Rastogi Aseem","year":"2012"},{"key":"e_1_2_2_34_1","volume-title":"Just-in-Time Static Type Checking for Dynamic Languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).","author":"Brianna"},{"key":"e_1_2_2_35_1","volume-title":"JSTrace: Run-time type discovery for JavaScript. Master\u2019s thesis","author":"Saftoiu Claudiu"},{"key":"e_1_2_2_36_1","volume-title":"Blame and Coercion: Together Again for the First Time. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).","author":"Siek Jeremy","year":"2015"},{"key":"e_1_2_2_37_1","unstructured":"Jeremy Siek Michael Vitousek Matteo Cimini and John Boyland. 2015. Refined Criteria for Gradual Typing. In Summit oN Advances in Programming Languages (SNAPL).  Jeremy Siek Michael Vitousek Matteo Cimini and John Boyland. 2015. Refined Criteria for Gradual Typing. In Summit oN Advances in Programming Languages (SNAPL)."},{"key":"e_1_2_2_38_1","volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (SW).","author":"Jeremy"},{"key":"e_1_2_2_39_1","volume-title":"Gradual Typing with Unification-based Inference. In Dynamic Languages Symposium (DLS).","author":"Jeremy"},{"key":"e_1_2_2_40_1","volume-title":"Monotonic References for Efficient Gradual Typing. In European Symposium on Programming (ESOP).","author":"Siek Jeremy G.","year":"2015"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_2_42_1","volume-title":"The Design and Implementation of Typed Scheme. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"Hochstadt Sam Tobin","year":"2008"},{"key":"e_1_2_2_43_1","volume-title":"European Conference on Object-Oriented Programming (ECOOP).","author":"Vekris Panagiotis","year":"2015"},{"key":"e_1_2_2_44_1","volume-title":"Design and Evaluation of Gradual Typing for Python. In Dynamic Languages Symposium (DLS).","author":"Vitousek Michael M.","year":"2014"},{"key":"e_1_2_2_45_1","volume-title":"Big Types in Little Runtime: Open-World Soundness and Collaborative Blame for Gradual Type Systems. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"Vitousek Michael M."},{"key":"e_1_2_2_46_1","volume-title":"International Conference on Learning Representations (ICLR).","author":"Wei Jiayi","year":"2020"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/239912.239917"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485488","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485488","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485488","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485488"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":46,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485488"],"URL":"https:\/\/doi.org\/10.1145\/3485488","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}