{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:20:29Z","timestamp":1750220429716,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,9,25]],"date-time":"2019-09-25T00:00:00Z","timestamp":1569369600000},"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":[[2019,9,25]]},"DOI":"10.1145\/3412932.3412940","type":"proceedings-article","created":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T16:08:45Z","timestamp":1626365325000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A space-efficient call-by-value virtual machine for gradual set-theoretic types"],"prefix":"10.1145","author":[{"given":"Giuseppe","family":"Castagna","sequence":"first","affiliation":[{"name":"CNRS"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Duboc","sequence":"additional","affiliation":[{"name":"ENS Lyon"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Lanvin","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Paris"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy G.","family":"Siek","sequence":"additional","affiliation":[{"name":"Indiana University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Sound gradual typing: Only mostly dead. PACMPL, 1(OOPSLA):54","author":"Bauman S.","year":"2017","unstructured":"S. Bauman , C. F. Bolz-Tereick , J. G. Siek , and S. Tobin-Hochstadt . Sound gradual typing: Only mostly dead. PACMPL, 1(OOPSLA):54 , 2017 . S. Bauman, C. F. Bolz-Tereick, J. G. Siek, and S. Tobin-Hochstadt. Sound gradual typing: Only mostly dead. PACMPL, 1(OOPSLA):54, 2017."},{"key":"e_1_3_2_1_2_1","first-page":"257","volume-title":"Understanding TypeScript. In European Conference on Object-Oriented Programming","author":"Bierman G.","year":"2014","unstructured":"G. Bierman , M. Abadi , and M. Torgersen . Understanding TypeScript. In European Conference on Object-Oriented Programming , pages 257 -- 281 . Springer , 2014 . G. Bierman, M. Abadi, and M. Torgersen. Understanding TypeScript. In European Conference on Object-Oriented Programming, pages 257--281. Springer, 2014."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_4"},{"key":"e_1_3_2_1_4_1","volume-title":"Logical Methods in Computer Science, 2019","author":"Castagna G.","year":"1809","unstructured":"G. Castagna . Covariance and controvariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers) . Logical Methods in Computer Science, 2019 . https:\/\/arxiv.org\/abs\/ 1809 .01427. To appear. G. Castagna. Covariance and controvariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers). Logical Methods in Computer Science, 2019. https:\/\/arxiv.org\/abs\/1809.01427. To appear."},{"key":"e_1_3_2_1_5_1","volume-title":"Gradual typing with union and intersection types. PACMPL, 1(ICFP):41","author":"Castagna G.","year":"2017","unstructured":"G. Castagna and V. Lanvin . Gradual typing with union and intersection types. PACMPL, 1(ICFP):41 , 2017 . G. Castagna and V. Lanvin. Gradual typing with union and intersection types. PACMPL, 1(ICFP):41, 2017."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1145\/2676726.2676991","volume-title":"POPL '15","volume":"50","author":"Castagna G.","year":"2015","unstructured":"G. Castagna , K. Nguyen , Z. Xu , and P. Abate . Polymorphic functions with set-theoretic types: Part 2: Local type inference and type reconstruction . In POPL '15 , volume 50 , pages 289 -- 302 , 2015 . G. Castagna, K. Nguyen, Z. Xu, and P. Abate. Polymorphic functions with set-theoretic types: Part 2: Local type inference and type reconstruction. In POPL '15, volume 50, pages 289--302, 2015."},{"key":"e_1_3_2_1_7_1","volume-title":"Gradual typing: a new perspective. PACMPL, 3(POPL):16","author":"Castagna G.","year":"2019","unstructured":"G. Castagna , V. Lanvin , T. Petrucciani , and J. G. Siek . Gradual typing: a new perspective. PACMPL, 3(POPL):16 , 2019 . G. Castagna, V. Lanvin, T. Petrucciani, and J. G. Siek. Gradual typing: a new perspective. PACMPL, 3(POPL):16, 2019."},{"key":"e_1_3_2_1_8_1","volume-title":"PLDI '98","author":"Clinger W.","year":"1998","unstructured":"W. Clinger . Proper tail recursion and space efficiency . In PLDI '98 , 1998 . W. Clinger. Proper tail recursion and space efficiency. In PLDI '98, 1998."},{"key":"e_1_3_2_1_9_1","unstructured":"Facebook. Flow documentation . https:\/\/flow.org\/en\/docs\/lang\/.  Facebook. Flow documentation . https:\/\/flow.org\/en\/docs\/lang\/."},{"key":"e_1_3_2_1_10_1","unstructured":"Facebook. Hack documentation . https:\/\/docs.hhvm.com\/hack\/.  Facebook. Hack documentation . https:\/\/docs.hhvm.com\/hack\/."},{"key":"e_1_3_2_1_11_1","first-page":"1","article-title":"Collapsible contracts: Fixing a pathology of gradual typing","volume":"133","author":"Feltey D.","year":"2018","unstructured":"D. Feltey , B. Greenman , C. Scholliers , R.B. Findler , and V. St-Amour . Collapsible contracts: Fixing a pathology of gradual typing . PACMPL, 2(OOPSLA) : 133 : 1 -- 133 :27, October 2018 . D. Feltey, B. Greenman, C. Scholliers, R.B. Findler, and V. St-Amour. Collapsible contracts: Fixing a pathology of gradual typing. PACMPL, 2(OOPSLA):133:1--133:27, October 2018.","journal-title":"PACMPL, 2(OOPSLA)"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1145\/581478.581484","volume-title":"ICFP '02","author":"Findler R. B.","year":"2002","unstructured":"R. B. Findler and M. Felleisen . Contracts for higher-order functions . In ICFP '02 , pages 48 -- 59 , October 2002 . R. B. Findler and M. Felleisen. Contracts for higher-order functions. In ICFP '02, pages 48--59, October 2002."},{"key":"e_1_3_2_1_13_1","volume-title":"Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM (JACM), 55(4):19","author":"Frisch Alain","year":"2008","unstructured":"Alain Frisch , Giuseppe Castagna , and V\u00e9ronique Benzaken . Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM (JACM), 55(4):19 , 2008 . Alain Frisch, Giuseppe Castagna, and V\u00e9ronique Benzaken. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM (JACM), 55(4):19, 2008."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/2676726.2676967","volume-title":"POPL '15","author":"Greenberg M.","year":"2015","unstructured":"M. Greenberg . Space-efficient manifest contracts . In POPL '15 , pages 181 -- 194 . ACM, 2015 . M. Greenberg. Space-efficient manifest contracts. In POPL '15, pages 181--194. ACM, 2015."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1145\/2784731.2784737","volume-title":"ICFP 2015","author":"Keil M.","year":"2015","unstructured":"M. Keil and P. Thiemann . Blame assignment for higher-order contracts with intersection and union . In ICFP 2015 , pages 375 -- 386 , 2015 . M. Keil and P. Thiemann. Blame assignment for higher-order contracts with intersection and union. In ICFP 2015, pages 375--386, 2015."},{"key":"e_1_3_2_1_18_1","volume-title":"PLDI '19","author":"Kuhlenschmidt A.","year":"2019","unstructured":"A. Kuhlenschmidt , D. Almahallawi , and J. G. Siek . Toward efficient gradual typing for structural types via coercions . In PLDI '19 , 2019 . A. Kuhlenschmidt, D. Almahallawi, and J. G. Siek. Toward efficient gradual typing for structural types via coercions. In PLDI '19, 2019."},{"key":"e_1_3_2_1_19_1","volume-title":"Workshop on Scripts to Programs (STOP)","author":"Lehtosalo J.","year":"2011","unstructured":"J. Lehtosalo and D. J. Greaves . Language with a pluggable type system and optional runtime monitoring of type errors . In Workshop on Scripts to Programs (STOP) , 2011 . J. Lehtosalo and D. J. Greaves. Language with a pluggable type system and optional runtime monitoring of type errors. In Workshop on Scripts to Programs (STOP), 2011."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1145\/2676726.2676971","volume-title":"POPL '15","author":"Rastogi A.","year":"2015","unstructured":"A. Rastogi , N. Swamy , C. Fournet , G. Bierman , and P. Vekris . Safe & efficient gradual typing for TypeScript . In POPL '15 , pages 167 -- 180 . ACM, 2015 . A. Rastogi, N. Swamy, C. Fournet, G. Bierman, and P. Vekris. Safe & efficient gradual typing for TypeScript. In POPL '15, pages 167--180. ACM, 2015."},{"key":"e_1_3_2_1_21_1","volume-title":"ECOOP 2015","author":"Richards G.","year":"2015","unstructured":"G. Richards , F. Zappa Nardelli , and J. Vitek . Concrete types for TypeScript . In ECOOP 2015 , 2015 . G. Richards, F. Zappa Nardelli, and J. Vitek. Concrete types for TypeScript. In ECOOP 2015, 2015."},{"key":"e_1_3_2_1_22_1","first-page":"68","volume-title":"Workshop on Scheme and Functional Programming","author":"Siek J. G.","year":"2012","unstructured":"J. G. Siek and R. Garcia . Interpretations of the gradually-typed lambda calculus . In Workshop on Scheme and Functional Programming , pages 68 -- 80 , 2012 . J. G. Siek and R. Garcia. Interpretations of the gradually-typed lambda calculus. In Workshop on Scheme and Functional Programming, pages 68--80, 2012."},{"key":"e_1_3_2_1_23_1","first-page":"81","volume-title":"Scheme and Functional Programming Workshop","volume":"6","author":"Siek J. G.","year":"2006","unstructured":"J. G. Siek and W. Taha . Gradual typing for functional languages . In Scheme and Functional Programming Workshop , volume 6 , pages 81 -- 92 , 2006 . J. G. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, volume 6, pages 81--92, 2006."},{"key":"e_1_3_2_1_24_1","first-page":"7","volume-title":"Symposium on Dynamic languages","author":"Siek J. G.","unstructured":"J. G. Siek and M. Vachharajani . Gradual typing with unification-based inference . In Symposium on Dynamic languages , page 7 . ACM, 2008. J. G. Siek and M. Vachharajani. Gradual typing with unification-based inference. In Symposium on Dynamic languages, page 7. ACM, 2008."},{"key":"e_1_3_2_1_25_1","first-page":"365","article-title":"Threesomes, with and without blame","volume":"2010","author":"Siek J. G.","year":"2010","unstructured":"J. G. Siek and P. Wadler . Threesomes, with and without blame . In POPL 2010 , pages 365 -- 376 , 2010 . J. G. Siek and P. Wadler. Threesomes, with and without blame. In POPL 2010, pages 365--376, 2010.","journal-title":"POPL"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1145\/2737924.2737968","volume-title":"PLDI '15","author":"Siek J. G.","year":"2015","unstructured":"J. G. Siek , P. Thiemann , and P. Wadler . Blame and coercion: together again for the first time . In PLDI '15 , pages 425 -- 435 , 2015 . J. G. Siek, P. Thiemann, and P. Wadler. Blame and coercion: together again for the first time. In PLDI '15, pages 425--435, 2015."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1145\/2837614.2837630","volume-title":"POPL '16","author":"Takikawa A.","year":"2016","unstructured":"A. Takikawa , D. Feltey , B. Greenman , M. S. New , J. Vitek , and M. Felleisen . Is sound gradual typing dead ? In POPL '16 , pages 456 -- 468 , 2016 . A. Takikawa, D. Feltey, B. Greenman, M. S. New, J. Vitek, and M. Felleisen. Is sound gradual typing dead? In POPL '16, pages 456--468, 2016."},{"key":"e_1_3_2_1_28_1","first-page":"964","volume-title":"DSL '06","author":"Tobin-Hochstadt S.","year":"2006","unstructured":"S. Tobin-Hochstadt and M. Felleisen . Interlanguage migration: from scripts to programs . In DSL '06 , pages 964 -- 974 . ACM, 2006 . S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: from scripts to programs. In DSL '06, pages 964--974. ACM, 2006."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1145\/1328438.1328486","volume-title":"POPL '08","author":"Tobin-Hochstadt Sam","year":"2008","unstructured":"Sam Tobin-Hochstadt and Matthias Felleisen . The design and implementation of Typed Scheme . In POPL '08 , pages 395 -- 406 . ACM, 2008 . Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of Typed Scheme. In POPL '08, pages 395--406. ACM, 2008."},{"key":"e_1_3_2_1_30_1","first-page":"45","volume-title":"DSL '14","author":"Vitousek M. M.","year":"2014","unstructured":"M. M. Vitousek , A. M. Kent , J. G. Siek , and J. Baker . Design and evaluation of gradual typing for Python . In DSL '14 , pages 45 -- 56 , 2014 . M. M. Vitousek, A. M. Kent, J. G. Siek, and J. Baker. Design and evaluation of gradual typing for Python. In DSL '14, pages 45--56, 2014."}],"event":{"name":"IFL '19: Implementation and Application of Functional Languages","acronym":"IFL '19","location":"Singapore Singapore"},"container-title":["Proceedings of the 31st Symposium on Implementation and Application of Functional Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3412932.3412940","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3412932.3412940","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:02Z","timestamp":1750193222000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3412932.3412940"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,25]]},"references-count":30,"alternative-id":["10.1145\/3412932.3412940","10.1145\/3412932"],"URL":"https:\/\/doi.org\/10.1145\/3412932.3412940","relation":{},"subject":[],"published":{"date-parts":[[2019,9,25]]},"assertion":[{"value":"2021-07-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}