{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:54:19Z","timestamp":1773809659177,"version":"3.50.1"},"reference-count":53,"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\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1763922,1846350"],"award-info":[{"award-number":["1763922,1846350"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"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>Gradually typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks at the boundaries between typed and untyped code. Unfortunately, performance studies have shown that the overhead of these checks can be disastrously high, calling into question the viability of sound gradual typing. In this paper, we show that by building on existing work on soft contract verification, we can reduce or eliminate this overhead.<\/jats:p>\n          <jats:p>Our key insight is that while untyped code cannot be trusted by a gradual type system, there is no need to consider only the worst case when optimizing a gradually typed program. Instead, we statically analyze the untyped portions of a gradually typed program to prove that almost all of the dynamic checks implied by gradual type boundaries cannot fail, and can be eliminated at compile time. Our analysis is modular, and can be applied to any portion of a program.<\/jats:p>\n          <jats:p>We evaluate this approach on a dozen existing gradually typed programs previously shown to have prohibitive performance overhead\u2014with a median overhead of 2.5\u00d7 and up to 80.6\u00d7 in the worst case\u2014and eliminate all overhead in most cases, suffering only 1.5\u00d7 overhead in the worst case.<\/jats:p>","DOI":"10.1145\/3434334","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Corpse reviver: sound and efficient gradual typing via contract verification"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4384-6351","authenticated-orcid":false,"given":"Cameron","family":"Moy","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}]},{"given":"Ph\u00fac C.","family":"Nguy\u1ec5n","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Sam","family":"Tobin-Hochstadt","sequence":"additional","affiliation":[{"name":"Indiana University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9201-6864","authenticated-orcid":false,"given":"David","family":"Van Horn","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177847"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3275519"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133878"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384592.2384601"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113469"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133872"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277719"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110256"},{"key":"e_1_2_1_10_1","volume-title":"Robert Bruce Findler, and Mathew Flat","author":"Felleisen Mathias","year":"2009","unstructured":"Mathias Felleisen , Robert Bruce Findler, and Mathew Flat . 2009 . Semantics Engineering with PLT Redex . Mathias Felleisen, Robert Bruce Findler, and Mathew Flat. 2009. Semantics Engineering with PLT Redex."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276503"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/316686.316703"},{"key":"e_1_2_1_14_1","unstructured":"Google Inc. 2018. Dart. ( 2018 ) h. ttps:\/\/dart.dev\/  Google Inc. 2018. Dart. ( 2018 ) h. ttps:\/\/dart.dev\/"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-14805-8_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236766"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3162066"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000217"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314627"},{"key":"e_1_2_1_22_1","unstructured":"Jukka Lehtosalo. 2017. MyPy: Optional Static Typing for Python. ( 2h0t1t7p ).:\/\/mypy-lang.org\/  Jukka Lehtosalo. 2017. MyPy: Optional Static Typing for Python. ( 2h0t1t7p ).:\/\/mypy-lang.org\/"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111057"},{"key":"e_1_2_1_24_1","unstructured":"Microsoft Corp. 2014. TypeScript Language Specification. ( 2014 ).http:\/\/www.typescriptlang.org  Microsoft Corp. 2014. TypeScript Language Specification. ( 2014 ).http:\/\/www.typescriptlang.org"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133880"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158139"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000216"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737971"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676971"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133879"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2015.76"},{"key":"e_1_2_1_33_1","volume-title":"Siek and Walid Taha","author":"Jeremy","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha . 2006 . Gradual Typing for Functional LanguagSecsh. eImne and Functional Programming Workshop . Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional LanguagSecsh. eImne and Functional Programming Workshop."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384685"},{"key":"e_1_2_1_37_1","unstructured":"Stripe Inc. 2019. Sorbet. ( 2019 ) h.ttps:\/\/sorbet.org\/  Stripe Inc. 2019. Sorbet. ( 2019 ) h.ttps:\/\/sorbet.org\/"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535889"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2015.4"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837630"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.17"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.8"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661088.2661101"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359619.3359742"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009849"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/239912.239917"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706343"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103767"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434334","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434334","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434334","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:47Z","timestamp":1750195907000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434334"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434334"],"URL":"https:\/\/doi.org\/10.1145\/3434334","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}