{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:54:12Z","timestamp":1773809652918,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":71,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523430","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"580-593","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Deep and shallow types for gradual languages"],"prefix":"10.1145","author":[{"given":"Ben","family":"Greenman","sequence":"first","affiliation":[{"name":"Brown University, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"251","article-title":"Confined gradual typing","author":"Allende Esteban","year":"2014","unstructured":"Esteban Allende , Johan Fabry , Ronald Garcia , and \u00c9ric Tanter . 2014 . Confined gradual typing . In OOPSLA , 251 - 270 . doi: 10.1145\/2660193.2660222. 10.1145\/2660193.2660222 Esteban Allende, Johan Fabry, Ronald Garcia, and \u00c9ric Tanter. 2014. Confined gradual typing. In OOPSLA, 251-270. doi: 10.1145\/2660193.2660222.","journal-title":"OOPSLA"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508168.2508171"},{"key":"e_1_3_2_1_3_1","first-page":"289","article-title":"Typing the numeric tower","author":"St-Amour Vincent","year":"2012","unstructured":"Vincent St-Amour , Sam Tobin-Hochstadt , Matthew Flatt , and Matthias Felleisen . 2012 . Typing the numeric tower . In PADL , 289 - 303 . doi: 10.1007\/978-3-642-27694-1_21. 10.1007\/978-3-642-27694-1_21 Vincent St-Amour, Sam Tobin-Hochstadt, Matthew Flatt, and Matthias Felleisen. 2012. Typing the numeric tower. In PADL, 289-303. doi: 10.1007\/978-3-642-27694-1_21.","journal-title":"PADL"},{"key":"e_1_3_2_1_4_1","unstructured":"Anonymous Author (s). 2022. Gradual soundness: lessons from Static Python. In Submitted for publication.   Anonymous Author (s). 2022. Gradual soundness: lessons from Static Python. In Submitted for publication."},{"key":"e_1_3_2_1_5_1","first-page":"1","article-title":"Sound gradual typing: only mostly dead","volume":"54","author":"Bauman Spenser","year":"2017","unstructured":"Spenser Bauman , Carl Friedrich Bolz-Tereick , Jeremy Siek , and Sam Tobin-Hochstadt . 2017 . Sound gradual typing: only mostly dead . PACMPL, 1, OOPSLA , 54 : 1 - 54 : 24. doi: 10.1145\/3133878. 10.1145\/3133878 Spenser Bauman, Carl Friedrich Bolz-Tereick, Jeremy Siek, and Sam Tobin-Hochstadt. 2017. Sound gradual typing: only mostly dead. PACMPL, 1, OOPSLA, 54 : 1-54 : 24. doi: 10.1145\/3133878.","journal-title":"PACMPL, 1, OOPSLA"},{"key":"e_1_3_2_1_6_1","first-page":"257","article-title":"Understanding TypeScript","author":"Bierman Gavin","year":"2014","unstructured":"Gavin Bierman , Martin Abadi , and Mads Torgersen . 2014 . Understanding TypeScript . In ECOOP , 257 - 281 . doi: 10.1007\/978-3-662-44 202-9_11. 10.1007\/978-3-662-44 Gavin Bierman, Martin Abadi, and Mads Torgersen. 2014. Understanding TypeScript. In ECOOP, 257-281. doi: 10.1007\/978-3-662-44 202-9_11.","journal-title":"ECOOP"},{"key":"e_1_3_2_1_7_1","first-page":"117","article-title":"Thorn: robust, concurrent, extensible scripting on the JVM","author":"Bloom Bard","year":"2009","unstructured":"Bard Bloom , John Field , Nathaniel Nystrom , Johan \u00d6stlund , Gregor Richards , Rok Strni\u0161a , Jan Vitek , and Tobias Wrigstad . 2009 . Thorn: robust, concurrent, extensible scripting on the JVM . In OOPSLA , 117 - 136 . doi: 10.1145\/1640089.1640098. 10.1145\/1640089.1640098 Bard Bloom, John Field, Nathaniel Nystrom, Johan \u00d6stlund, Gregor Richards, Rok Strni\u0161a, Jan Vitek, and Tobias Wrigstad. 2009. Thorn: robust, concurrent, extensible scripting on the JVM. In OOPSLA, 117-136. doi: 10.1145\/1640089.1640098.","journal-title":"OOPSLA"},{"key":"#cr-split#-e_1_3_2_1_8_1.1","doi-asserted-by":"crossref","unstructured":"Giuseppe Castagna and Victor Lanvin. 2017. Gradual typing with union and intersection types. PACMPL 1 ICFP 41 : 1-41 : 28. doi: 10.1145\/3110285. 10.1145\/3110285","DOI":"10.1145\/3110285"},{"key":"#cr-split#-e_1_3_2_1_8_1.2","doi-asserted-by":"crossref","unstructured":"Giuseppe Castagna and Victor Lanvin. 2017. Gradual typing with union and intersection types. PACMPL 1 ICFP 41 : 1-41 : 28. doi: 10.1145\/3110285.","DOI":"10.1145\/3110285"},{"key":"e_1_3_2_1_9_1","first-page":"1","article-title":"KafKa: gradual typing for objects","volume":"12","author":"Chung Benjamin","year":"2018","unstructured":"Benjamin Chung , Paley Li , Francesco Zappa Nardelli , and Jan Vitek . 2018 . KafKa: gradual typing for objects . In ECOOP , 12 : 1 - 12 : 23. doi: 10.4230\/LIPIcs.ECOOP. 2018. 12. 10.4230\/LIPIcs.ECOOP Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek. 2018. KafKa: gradual typing for objects. In ECOOP, 12 : 1-12 : 23. doi: 10.4230\/LIPIcs.ECOOP. 2018. 12.","journal-title":"ECOOP"},{"key":"e_1_3_2_1_10_1","first-page":"1","volume-title":"SFP. Universit\u00e9 Laval, DIUL-RT-0701","author":"Culpepper Ryan","year":"2007","unstructured":"Ryan Culpepper , Sam Tobin-Hochstadt , and Matthew Flatt . 2007. Advanced macrology and the implementation of Typed Scheme . In SFP. Universit\u00e9 Laval, DIUL-RT-0701 , 1 - 14 . http:\/\/www2.ift.ulaval.ca \/~dadub100\/sfp 2007 \/procPaper1.pdf. Ryan Culpepper, Sam Tobin-Hochstadt, and Matthew Flatt. 2007. Advanced macrology and the implementation of Typed Scheme. In SFP. Universit\u00e9 Laval, DIUL-RT-0701, 1-14. http:\/\/www2.ift.ulaval.ca \/~dadub100\/sfp2007\/procPaper1.pdf."},{"key":"e_1_3_2_1_11_1","first-page":"475","article-title":"Option contracts","author":"Dimoulas Christos","year":"2013","unstructured":"Christos Dimoulas , Robert Bruce Findler , and Matthias Felleisen . 2013 . Option contracts . In OOPSLA , 475 - 494 . doi: 10.1145\/2509136.2 509548. 10.1145\/2509136.2 Christos Dimoulas, Robert Bruce Findler, and Matthias Felleisen. 2013. Option contracts. In OOPSLA, 475-494. doi: 10.1145\/2509136.2 509548.","journal-title":"OOPSLA"},{"key":"e_1_3_2_1_12_1","first-page":"214","article-title":"Complete monitors for behavioral contracts","author":"Dimoulas Christos","year":"2012","unstructured":"Christos Dimoulas , Sam Tobin-Hochstadt , and Matthias Felleisen . 2012 . Complete monitors for behavioral contracts . In ESOP , 214 - 233 . doi: 10.1007\/978-3-642-28869-2_11. 10.1007\/978-3-642-28869-2_11 Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Complete monitors for behavioral contracts. In ESOP, 214-233. doi: 10.1007\/978-3-642-28869-2_11.","journal-title":"ESOP"},{"key":"e_1_3_2_1_13_1","volume-title":"Robert Bruce Findler, and Matthew Flatt","author":"Felleisen Matthias","year":"2009","unstructured":"Matthias Felleisen , Robert Bruce Findler, and Matthew Flatt . 2009 . Semantics Engineering with PLT Redex. MIT Press . isbn: 978-0-262-06275-6. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. MIT Press. isbn: 978-0-262-06275-6."},{"key":"e_1_3_2_1_14_1","first-page":"1","article-title":"Collapsible contracts: fixing a pathology of gradual typing","volume":"133","author":"Feltey Daniel","year":"2018","unstructured":"Daniel Feltey , Ben Greenman , Christophe Scholliers , Robert Bruce Findler , and Vincent St-Amour . 2018 . Collapsible contracts: fixing a pathology of gradual typing . PACMPL, 2, OOPSLA , 133 : 1 - 133 : 27. doi: 10.1145\/3276503. 10.1145\/3276503 Daniel Feltey, Ben Greenman, Christophe Scholliers, Robert Bruce Findler, and Vincent St-Amour. 2018. Collapsible contracts: fixing a pathology of gradual typing. PACMPL, 2, OOPSLA, 133 : 1-133 : 27. doi: 10.1145\/3276503.","journal-title":"PACMPL, 2, OOPSLA"},{"key":"e_1_3_2_1_15_1","volume-title":"Contracts as Pairs of Projections. Tech. rep. TR-2006-01","author":"Findler Robert Bruce","unstructured":"Robert Bruce Findler and Matthias Blume . 2006. Contracts as Pairs of Projections. Tech. rep. TR-2006-01 . University of Chicago . doi: 10.1007\/11737414_16. 10.1007\/11737414_16 Robert Bruce Findler and Matthias Blume. 2006. Contracts as Pairs of Projections. Tech. rep. TR-2006-01. University of Chicago. doi: 10.1007\/11737414_16."},{"key":"e_1_3_2_1_16_1","first-page":"48","article-title":"Contracts for higher-order functions","author":"Findler Robert Bruce","year":"2002","unstructured":"Robert Bruce Findler and Matthias Felleisen . 2002 . Contracts for higher-order functions . In ICFP , 48 - 59 . doi: 10.1145\/581478.581484. 10.1145\/581478.581484 Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for higher-order functions. In ICFP, 48-59. doi: 10.1145\/581478.581484.","journal-title":"ICFP"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837620"},{"key":"e_1_3_2_1_18_1","first-page":"13","article-title":"Submodules in Racket: you want it When, again","author":"Flatt Matthew","year":"2013","unstructured":"Matthew Flatt . 2013 . Submodules in Racket: you want it When, again ? In GPSE , 13 - 22 . doi: 10.1145\/2517208.2517211. 10.1145\/2517208.2517211 Matthew Flatt. 2013. Submodules in Racket: you want it When, again ? In GPSE, 13-22. doi: 10.1145\/2517208.2517211.","journal-title":"GPSE"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000093"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676967"},{"key":"e_1_3_2_1_23_1","volume-title":"Deep and Shallow Types for Gradual Languages (source code) version 1.0","author":"Rel SW","year":"2022","unstructured":"[ SW Rel . ] Ben Greenman , Deep and Shallow Types for Gradual Languages (source code) version 1.0 , 2022 . vcs: https:\/\/github.com \/bennn\/g-pldi-2022, swhid: \u27e8swh:1:dir:2f1f76cafb72491d8526d18ae 556499065ac6853\u27e9. [SW Rel. ] Ben Greenman, Deep and Shallow Types for Gradual Languages (source code) version 1.0, 2022. vcs: https:\/\/github.com \/bennn\/g-pldi-2022, swhid: \u27e8swh:1:dir:2f1f76cafb72491d8526d18ae 556499065ac6853\u27e9."},{"key":"e_1_3_2_1_24_1","volume-title":"Apr.","author":"Greenman Ben","year":"2022","unstructured":"[SW] Ben Greenman , Deep and Shallow Types for Gradual Languages v1.0 version 1.0 , Apr. 2022 . doi: 10.5281\/zenodo.6498926. 10.5281\/zenodo.6498926 [SW] Ben Greenman, Deep and Shallow Types for Gradual Languages v1.0 version 1.0, Apr. 2022. doi: 10.5281\/zenodo.6498926."},{"key":"e_1_3_2_1_25_1","unstructured":"Ben Greenman and Matthias Felleisen. 2018. A spectrum of type soundness and performance. PACMPL 2 ICFP 71 : 1-71 : 32. doi: 10.1 145\/3236766.   Ben Greenman and Matthias Felleisen. 2018. A spectrum of type soundness and performance. PACMPL 2 ICFP 71 : 1-71 : 32. doi: 10.1 145\/3236766."},{"key":"e_1_3_2_1_26_1","first-page":"1","article-title":"Complete monitors for gradual types","volume":"122","author":"Greenman Ben","year":"2019","unstructured":"Ben Greenman , Matthias Felleisen , and Christos Dimoulas . 2019 . Complete monitors for gradual types . PACMPL, 3, OOPSLA , 122 : 1 - 122 : 29. doi: 10.1145\/3360548. 10.1145\/3360548 Ben Greenman, Matthias Felleisen, and Christos Dimoulas. 2019. Complete monitors for gradual types. PACMPL, 3, OOPSLA, 122 : 1-122 : 29. doi: 10.1145\/3360548.","journal-title":"PACMPL, 3, OOPSLA"},{"key":"#cr-split#-e_1_3_2_1_27_1.1","doi-asserted-by":"crossref","unstructured":"Ben Greenman Lukas Lazarek Christos Dimoulas and Matthias Felleisen. 2022. A transient semantics for Typed Racket. <Programming> 6 2 9 : 1-9 : 26. doi: 10.22152\/programming-journal.org\/ 2022 \/6\/9. 10.22152\/programming-journal.org","DOI":"10.22152\/programming-journal.org\/2022\/6\/9"},{"key":"#cr-split#-e_1_3_2_1_27_1.2","doi-asserted-by":"crossref","unstructured":"Ben Greenman Lukas Lazarek Christos Dimoulas and Matthias Felleisen. 2022. A transient semantics for Typed Racket. <Programming> 6 2 9 : 1-9 : 26. doi: 10.22152\/programming-journal.org\/ 2022 \/6\/9.","DOI":"10.22152\/programming-journal.org\/2022\/6\/9"},{"key":"e_1_3_2_1_28_1","first-page":"30","article-title":"On the cost of type-tag soundness","author":"Greenman Ben","year":"2018","unstructured":"Ben Greenman and Zeina Migeed . 2018 . On the cost of type-tag soundness . In PEPM , 30 - 39 . doi: 10.1145\/3162066. 10.1145\/3162066 Ben Greenman and Zeina Migeed. 2018. On the cost of type-tag soundness. In PEPM, 30-39. doi: 10.1145\/3162066.","journal-title":"PEPM"},{"key":"e_1_3_2_1_29_1","first-page":"1","article-title":"How to evaluate the performance of gradual type systems","volume":"29","author":"Greenman Ben","year":"2019","unstructured":"Ben Greenman , Asumu Takikawa , Max S. New , Daniel Feltey , Robert Bruce Findler , Jan Vitek , and Matthias Felleisen . 2019 . How to evaluate the performance of gradual type systems . JFP , 29 , e4, 1 - 45 . doi: 10.1017\/S0956796818000217. 10.1017\/S0956796818000217 Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, Robert Bruce Findler, Jan Vitek, and Matthias Felleisen. 2019. How to evaluate the performance of gradual type systems. JFP, 29, e4, 1-45. doi: 10.1017\/S0956796818000217.","journal-title":"JFP"},{"key":"e_1_3_2_1_30_1","volume-title":"Sage: hybrid checking for flexible speciifcations","author":"Gronski Jessica","year":"2006","unstructured":"Jessica Gronski , Kenneth Knowles , Aaron Tomb , Stephen N. Freund , and Cormac Flanagan . 2006. Sage: hybrid checking for flexible speciifcations . In SFP. University of Chicago , TR- 2006 -06, 93-104. http:\/\/sc heme2006. cs.uchicago.edu\/scheme2006.pdf. Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. 2006. Sage: hybrid checking for flexible speciifcations. In SFP. University of Chicago, TR-2006-06, 93-104. http:\/\/sc heme2006. cs.uchicago.edu\/scheme2006.pdf."},{"key":"e_1_3_2_1_31_1","volume-title":"GTP Benchmarks version 6.0","author":"Rel SW","year":"2020","unstructured":"[ SW Rel .] , GTP Benchmarks version 6.0 , 2020 . vcs: https:\/\/github.co m\/bennn\/gtp-benchmarks, swhid: \u27e8swh:1:rev:d1a85945b64d8f4987 6f8921ef7a7bcdd82cc96f \u27e9. [SW Rel.], GTP Benchmarks version 6.0, 2020. vcs: https:\/\/github.co m\/bennn\/gtp-benchmarks, swhid: \u27e8swh:1:rev:d1a85945b64d8f4987 6f8921ef7a7bcdd82cc96f \u27e9."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297081.1297089"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"issue":"2","key":"e_1_3_2_1_34_1","first-page":"167","article-title":"Spaceeficient gradual typing","volume":"23","author":"Herman David","year":"2010","unstructured":"David Herman , Aaron Tomb , and Cormac Flanagan . 2010 . Spaceeficient gradual typing . HOSC , 23 , 2 , 167 - 189 . doi: 10.1007\/s10990-011-9066-z. 10.1007\/s10990-011-9066-z David Herman, Aaron Tomb, and Cormac Flanagan. 2010. Spaceeficient gradual typing. HOSC, 23, 2, 167-189. doi: 10.1007\/s10990-011-9066-z.","journal-title":"HOSC"},{"key":"e_1_3_2_1_35_1","first-page":"804","article-title":"Sums of uncertainty: refinements go gradual","author":"Jafery Khurram A.","year":"2017","unstructured":"Khurram A. Jafery and Jana Dunfield . 2017 . Sums of uncertainty: refinements go gradual . In POPL , 804 - 817 . doi: 10.1145\/3009837.300 9865. 10.1145\/3009837.300 Khurram A. Jafery and Jana Dunfield. 2017. Sums of uncertainty: refinements go gradual. In POPL, 804-817. doi: 10.1145\/3009837.300 9865.","journal-title":"POPL"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784737"},{"key":"e_1_3_2_1_37_1","first-page":"517","article-title":"Toward eficient gradual typing for structural types via coercions","author":"Kuhlenschmidt Andre","year":"2019","unstructured":"Andre Kuhlenschmidt , Deyaaeldeen Almahallawi , and Jeremy G. Siek . 2019 . Toward eficient gradual typing for structural types via coercions . In PLDI , 517 - 532 . doi: 10.1145\/3314221.3314627. 10.1145\/3314221.3314627 Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G. Siek. 2019. Toward eficient gradual typing for structural types via coercions. In PLDI, 517-532. doi: 10.1145\/3314221.3314627.","journal-title":"PLDI"},{"key":"#cr-split#-e_1_3_2_1_38_1.1","doi-asserted-by":"crossref","unstructured":"Lukas Lazarek Ben Greenman Matthias Felleisen and Christos Dimoulas. 2021. How to evaluate blame for gradual types. PACMPL 5 ICFP 68 : 1-68 : 29. doi: 10.1145\/3473573. 10.1145\/3473573","DOI":"10.1145\/3473573"},{"key":"#cr-split#-e_1_3_2_1_38_1.2","doi-asserted-by":"crossref","unstructured":"Lukas Lazarek Ben Greenman Matthias Felleisen and Christos Dimoulas. 2021. How to evaluate blame for gradual types. PACMPL 5 ICFP 68 : 1-68 : 29. doi: 10.1145\/3473573.","DOI":"10.1145\/3473573"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498930"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_1_41_1","first-page":"1","article-title":"Corpse reviver: sound and eficient gradual typing via contract verification","author":"Moy Cameron","year":"2021","unstructured":"Cameron Moy , Phuc C. Nguyen , Sam Tobin-Hochstadt , and David Van Horn . 2021 . Corpse reviver: sound and eficient gradual typing via contract verification . PACMPL, 5, POPL , 1 - 28 . doi: 10.1145\/3434 334. 10.1145\/3434 Cameron Moy, Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn. 2021. Corpse reviver: sound and eficient gradual typing via contract verification. PACMPL, 5, POPL, 1-28. doi: 10.1145\/3434 334.","journal-title":"PACMPL, 5, POPL"},{"key":"e_1_3_2_1_42_1","first-page":"1","article-title":"Sound gradual typing is nominally alive and well","volume":"56","author":"Muehlboeck Fabian","year":"2017","unstructured":"Fabian Muehlboeck and Ross Tate . 2017 . Sound gradual typing is nominally alive and well . PACMPL, 1, OOPSLA , 56 : 1 - 56 : 30. doi: 10.1145\/3133880. 10.1145\/3133880 Fabian Muehlboeck and Ross Tate. 2017. Sound gradual typing is nominally alive and well. PACMPL, 1, OOPSLA, 56 : 1-56 : 30. doi: 10.1145\/3133880.","journal-title":"PACMPL, 1, OOPSLA"},{"key":"e_1_3_2_1_43_1","first-page":"1","article-title":"Transitioning from structural to nominal code with eficient gradual typing","volume":"127","author":"Muehlboeck Fabian","year":"2021","unstructured":"Fabian Muehlboeck and Ross Tate . 2021 . Transitioning from structural to nominal code with eficient gradual typing . PACMPL, 5, OOPSLA , 127 : 1 - 127 : 29. doi: 10.1145\/3485504. 10.1145\/3485504 Fabian Muehlboeck and Ross Tate. 2021. Transitioning from structural to nominal code with eficient gradual typing. PACMPL, 5, OOPSLA, 127 : 1-127 : 29. doi: 10.1145\/3485504.","journal-title":"PACMPL, 5, OOPSLA"},{"key":"e_1_3_2_1_44_1","first-page":"845","article-title":"Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs","author":"Nguyen Phuc C.","year":"2019","unstructured":"Phuc C. Nguyen , Thomas Gilray , Sam Tobin-Hochstadt , and David Van Horn . 2019 . Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs . In PLDI , 845 - 859 . doi: 10.1145\/3314221.3314643. 10.1145\/3314221.3314643 Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn. 2019. Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs. In PLDI, 845-859. doi: 10.1145\/3314221.3314643.","journal-title":"PLDI"},{"key":"e_1_3_2_1_45_1","first-page":"1","article-title":"Soft contract verification for higher-order stateful programs","volume":"51","author":"Nguyen Phuc C.","year":"2018","unstructured":"Phuc C. Nguyen , Thomas Gilray , Sam Tobin-Hochstadt , and David Van Horn . 2018 . Soft contract verification for higher-order stateful programs . PACMPL, 2, POPL , 51 : 1 - 51 : 30. doi: 10.1145\/3158139. 10.1145\/3158139 Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn. 2018. Soft contract verification for higher-order stateful programs. PACMPL, 2, POPL, 51 : 1-51 : 30. doi: 10.1145\/3158139.","journal-title":"PACMPL, 2, POPL"},{"key":"e_1_3_2_1_46_1","volume-title":"Racket version 7.8.0.5+ revision 7c9038","author":"Rel SW","year":"2020","unstructured":"[ SW Rel .] , Racket version 7.8.0.5+ revision 7c9038 , 2020 . vcs: https: \/\/github.com\/racket\/racket, swhid: \u27e8 swh:1:rev:7c903871bd8cb4bd32 ed7188c180b5124f9bc201\u27e9. [SW Rel.], Racket version 7.8.0.5+ revision 7c9038, 2020. vcs: https: \/\/github.com\/racket\/racket, swhid: \u27e8 swh:1:rev:7c903871bd8cb4bd32 ed7188c180b5124f9bc201\u27e9."},{"key":"e_1_3_2_1_47_1","first-page":"1","article-title":"The vm already knew that: leveraging compile-time knowledge to optimize gradual typing","volume":"55","author":"Richards Gregor","year":"2017","unstructured":"Gregor Richards , Ellen Arteca , and Alexi Turcotte . 2017 . The vm already knew that: leveraging compile-time knowledge to optimize gradual typing . PACMPL, 1, OOPSLA , 55 : 1 - 55 : 27. doi: 10.1145\/31338 79. 10.1145\/31338 Gregor Richards, Ellen Arteca, and Alexi Turcotte. 2017. The vm already knew that: leveraging compile-time knowledge to optimize gradual typing. PACMPL, 1, OOPSLA, 55 : 1-55 : 27. doi: 10.1145\/31338 79.","journal-title":"PACMPL, 1, OOPSLA"},{"key":"e_1_3_2_1_48_1","first-page":"76","article-title":"Concrete types for TypeScript","author":"Richards Gregor","year":"2015","unstructured":"Gregor Richards , Francesco Zappa Nardelli , and Jan Vitek . 2015 . Concrete types for TypeScript . In ECOOP , 76 - 100 . doi: 10.4230\/LIPIc s. ECOOP. 2015. 76. 10.4230\/LIPIc Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. 2015. Concrete types for TypeScript. In ECOOP, 76-100. doi: 10.4230\/LIPIc s. ECOOP. 2015. 76.","journal-title":"ECOOP"},{"key":"e_1_3_2_1_49_1","first-page":"1","article-title":"Transient typechecks are (almost) free","volume":"15","author":"Roberts Richard","year":"2019","unstructured":"Richard Roberts , Stefan Marr , Michael Homer , and James Noble . 2019 . Transient typechecks are (almost) free . In ECOOP , 15 : 1 - 15 : 29. doi: 10.4230\/LIPIcs.ECOOP. 2019. 5. 10.4230\/LIPIcs.ECOOP Richard Roberts, Stefan Marr, Michael Homer, and James Noble. 2019. Transient typechecks are (almost) free. In ECOOP, 15 : 1-15 : 29. doi: 10.4230\/LIPIcs.ECOOP. 2019. 5.","journal-title":"ECOOP"},{"key":"e_1_3_2_1_50_1","volume-title":"Siek and Walid Taha","author":"Jeremy","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha . 2006 . Gradual typing for functional languages. In SFP. University of Chicago , TR-2006-06, 81-92. http:\/\/sc heme2006. cs.uchicago.edu\/scheme2006.pdf. Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In SFP. University of Chicago, TR-2006-06, 81-92. http:\/\/sc heme2006. cs.uchicago.edu\/scheme2006.pdf."},{"key":"e_1_3_2_1_51_1","first-page":"e20","article-title":"Blame and coercion: together again for the first time","volume":"31","author":"Siek Jeremy G.","year":"2021","unstructured":"Jeremy G. Siek , Peter Thiemann , and Philip Wadler . 2021 . Blame and coercion: together again for the first time . JFP , 31 , e20 . doi: 10.1017\/S0956796821000101. 10.1017\/S0956796821000101 Jeremy G. Siek, Peter Thiemann, and Philip Wadler. 2021. Blame and coercion: together again for the first time. JFP, 31, e20. doi: 10.1017\/S0956796821000101.","journal-title":"JFP"},{"key":"e_1_3_2_1_52_1","first-page":"274","article-title":"Refined criteria for gradual typing","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek , Michael M. Vitousek , Matteo Cimini , and John Tang Boyland . 2015 . Refined criteria for gradual typing . In SNAPL , 274 - 293 . doi: 10.4230\/LIPIcs.SNAPL. 2015. 274. 10.4230\/LIPIcs.SNAPL Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined criteria for gradual typing. In SNAPL, 274-293. doi: 10.4230\/LIPIcs.SNAPL. 2015. 274.","journal-title":"SNAPL"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737968"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384685"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837630"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384674"},{"key":"e_1_3_2_1_57_1","first-page":"132","article-title":"Languages as libraries","author":"Tobin-Hochstadt Sam","year":"2011","unstructured":"Sam Tobin-Hochstadt , Vincent St-Amour , Ryan Culpepper , Matthew Flatt , and Matthias Felleisen . 2011 . Languages as libraries . In PLDI , 132 - 141 . doi: 10.1145\/1993498.1993514. 10.1145\/1993498.1993514 Sam Tobin-Hochstadt, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, and Matthias Felleisen. 2011. Languages as libraries. In PLDI, 132-141. doi: 10.1145\/1993498.1993514.","journal-title":"PLDI"},{"key":"e_1_3_2_1_58_1","first-page":"964","article-title":"Interlanguage migration: from scripts to programs","author":"Tobin-Hochstadt Sam","year":"2006","unstructured":"Sam Tobin-Hochstadt and Matthias Felleisen . 2006 . Interlanguage migration: from scripts to programs . In DLS , 964 - 974 . doi: 10.1145\/1 176617.1176755. 10.1145\/1 Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage migration: from scripts to programs. In DLS, 964-974. doi: 10.1145\/1 176617.1176755.","journal-title":"DLS"},{"key":"e_1_3_2_1_59_1","first-page":"117","article-title":"Logical types for untyped languages","author":"Tobin-Hochstadt Sam","year":"2010","unstructured":"Sam Tobin-Hochstadt and Matthias Felleisen . 2010 . Logical types for untyped languages . In ICFP , 117 - 128 . doi: 10.1145\/1863543.1863561. 10.1145\/1863543.1863561 Sam Tobin-Hochstadt and Matthias Felleisen. 2010. Logical types for untyped languages. In ICFP, 117-128. doi: 10.1145\/1863543.1863561.","journal-title":"ICFP"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1145\/1328438.1328486","article-title":"The design and implementation of Typed Scheme","author":"Tobin-Hochstadt Sam","year":"2008","unstructured":"Sam Tobin-Hochstadt and Matthias Felleisen . 2008 . The design and implementation of Typed Scheme . In POPL , 395 - 406 . doi: 10.1145\/1 328438.1328486. 10.1145\/1 Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The design and implementation of Typed Scheme. In POPL, 395-406. doi: 10.1145\/1 328438.1328486.","journal-title":"POPL"},{"key":"e_1_3_2_1_61_1","first-page":"1","article-title":"Migratory typing: ten years later","volume":"17","author":"Tobin-Hochstadt Sam","year":"2017","unstructured":"Sam Tobin-Hochstadt , Matthias Felleisen , Robert Bruce Findler , Matthew Flatt , Ben Greenman , Andrew M. Kent , Vincent St-Amour , T. Stephen Strickland , and Asumu Takikawa . 2017 . Migratory typing: ten years later . In SNAPL , 17 : 1 - 17 : 17. doi: 10.4230\/LIPIcs.SNAPL. 2017. 17. 10.4230\/LIPIcs.SNAPL Sam Tobin-Hochstadt, Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. 2017. Migratory typing: ten years later. In SNAPL, 17 : 1-17 : 17. doi: 10.4230\/LIPIcs.SNAPL. 2017. 17.","journal-title":"SNAPL"},{"key":"e_1_3_2_1_62_1","first-page":"382","article-title":"A gradual interpretation of union types","author":"Toro Mat\u00edas","year":"2017","unstructured":"Mat\u00edas Toro and \u00c9ric Tanter . 2017 . A gradual interpretation of union types . In SAS , 382 - 404 . doi: 10.1007\/978-3-319-66706-5_19. 10.1007\/978-3-319-66706-5_19 Mat\u00edas Toro and \u00c9ric Tanter. 2017. A gradual interpretation of union types. In SAS, 382-404. doi: 10.1007\/978-3-319-66706-5_19.","journal-title":"SAS"},{"key":"e_1_3_2_1_63_1","first-page":"1","article-title":"The behavior of gradual types: a user study","author":"Wilson Preston Tunnell","year":"2018","unstructured":"Preston Tunnell Wilson , Ben Greenman , Justin Pombrio , and Shriram Krishnamurthi . 2018 . The behavior of gradual types: a user study . In DLS , 1 - 12 . doi: 10.1145\/3276945.3276947. 10.1145\/3276945.3276947 Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi. 2018. The behavior of gradual types: a user study. In DLS, 1-12. doi: 10.1145\/3276945.3276947.","journal-title":"DLS"},{"key":"e_1_3_2_1_64_1","volume-title":"Typed Racket version 1.12+ revision c074c93","author":"Rel SW","year":"2020","unstructured":"[ SW Rel .] , Typed Racket version 1.12+ revision c074c93 , 2020 . vcs: https:\/\/github.com\/bennn\/typed-racket, swhid: \u27e8swh:1:rev:c074c93 33e467cb7cd2058511ac63a1d51b4948e\u27e9. [SW Rel.], Typed Racket version 1.12+ revision c074c93, 2020. vcs: https:\/\/github.com\/bennn\/typed-racket, swhid: \u27e8swh:1:rev:c074c93 33e467cb7cd2058511ac63a1d51b4948e\u27e9."},{"key":"e_1_3_2_1_65_1","first-page":"154","article-title":"Trustworthy proxies","author":"Cutsem Tom Van","year":"2013","unstructured":"Tom Van Cutsem and Mark S Miller . 2013 . Trustworthy proxies . In ECOOP , 154 - 178 . doi: 10.1007\/978-3-642-39038-8_7. 10.1007\/978-3-642-39038-8_7 Tom Van Cutsem and Mark S Miller. 2013. Trustworthy proxies. In ECOOP, 154-178. doi: 10.1007\/978-3-642-39038-8_7.","journal-title":"ECOOP"},{"key":"e_1_3_2_1_66_1","first-page":"45","article-title":"Design and evaluation of gradual typing for Python","author":"Vitousek Michael M.","year":"2014","unstructured":"Michael M. Vitousek , Andrew Kent , Jeremy G. Siek , and Jim Baker . 2014 . Design and evaluation of gradual typing for Python . In DLS , 45 - 56 . doi: 10.1145\/2661088.2661101. 10.1145\/2661088.2661101 Michael M. Vitousek, Andrew Kent, Jeremy G. Siek, and Jim Baker. 2014. Design and evaluation of gradual typing for Python. In DLS, 45-56. doi: 10.1145\/2661088.2661101.","journal-title":"DLS"},{"key":"e_1_3_2_1_67_1","first-page":"28","article-title":"Optimizing and evaluating transient gradual typing","author":"Vitousek Michael M.","year":"2019","unstructured":"Michael M. Vitousek , Jeremy G. Siek , and Avik Chaudhuri . 2019 . Optimizing and evaluating transient gradual typing . In DLS , 28 - 41 . doi: 10.1145\/3359619.3359742. 10.1145\/3359619.3359742 Michael M. Vitousek, Jeremy G. Siek, and Avik Chaudhuri. 2019. Optimizing and evaluating transient gradual typing. In DLS, 28-41. doi: 10.1145\/3359619.3359742.","journal-title":"DLS"},{"key":"e_1_3_2_1_68_1","first-page":"762","article-title":"Big types in little runtime: open-world soundness and collaborative blame for gradual type systems","author":"Vitousek Michael M.","year":"2017","unstructured":"Michael M. Vitousek , Cameron Swords , and Jeremy G. Siek . 2017 . Big types in little runtime: open-world soundness and collaborative blame for gradual type systems . In POPL , 762 - 774 . doi: 10.1145\/300 9837.3009849. 10.1145\/300 Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. 2017. Big types in little runtime: open-world soundness and collaborative blame for gradual type systems. In POPL, 762-774. doi: 10.1145\/300 9837.3009849.","journal-title":"POPL"},{"key":"e_1_3_2_1_70_1","first-page":"377","article-title":"Integrating typed and untyped code in a scripting language","author":"Wrigstad Tobias","year":"2010","unstructured":"Tobias Wrigstad , Francesco Zappa Nardelli , Sylvain Lebresne , Johan \u00d6stlund , and Jan Vitek . 2010 . Integrating typed and untyped code in a scripting language . In POPL , 377 - 388 . doi: 10.1145\/1706299.1706343. 10.1145\/1706299.1706343 Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan \u00d6stlund, and Jan Vitek. 2010. Integrating typed and untyped code in a scripting language. In POPL, 377-388. doi: 10.1145\/1706299.1706343.","journal-title":"POPL"}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"San Diego CA USA","acronym":"PLDI '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523430","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523430","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:31:16Z","timestamp":1750188676000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523430"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":71,"alternative-id":["10.1145\/3519939.3523430","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523430","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}