{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:17:40Z","timestamp":1781893060247,"version":"3.54.5"},"reference-count":88,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1518844"],"award-info":[{"award-number":["CCF-1518844"]}],"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":[[2018,7,30]]},"abstract":"<jats:p>The literature on gradual typing presents three fundamentally different ways of thinking about the integrity of programs that combine statically typed and dynamically typed code. This paper presents a uniform semantic framework that explains all three approaches, illustrates how each approach affects a developer's work, and adds a systematic performance comparison for a single implementation platform.<\/jats:p>","DOI":"10.1145\/3236766","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["A spectrum of type soundness and performance"],"prefix":"10.1145","volume":"2","author":[{"given":"Ben","family":"Greenman","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthias","family":"Felleisen","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103138"},{"key":"e_1_2_2_2_1","first-page":"214","volume-title":"Philip Wadler. Blame for All. Symposium on Principles of Programming Languages","author":"Ahmed Amal","year":"2011","unstructured":"Amal Ahmed , Robert Bruce Findler , Jeremy G. Siek , and Philip Wadler. Blame for All. Symposium on Principles of Programming Languages , pp. 201\u2013 214 , 2011 . Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for All. Symposium on Principles of Programming Languages, pp. 201\u2013214, 2011."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177847"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.06.006"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660222"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508168.2508171"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_19"},{"key":"e_1_2_2_8_1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt Henk","year":"1981","unstructured":"Henk Barendregt . The Lambda Calculus: Its Syntax and Semantics . North-Holland Publishing Company , 1981 . Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland Publishing Company, 1981."},{"key":"e_1_2_2_9_1","first-page":"15","volume-title":"Barthe. Implicit Coercions in Type Systems. International Workshop on Types for Proofs and Programs","author":"Gilles","year":"1995","unstructured":"Gilles Barthe. Implicit Coercions in Type Systems. International Workshop on Types for Proofs and Programs , pp. 1\u2013 15 , 1995 . Gilles Barthe. Implicit Coercions in Type Systems. International Workshop on Types for Proofs and Programs, pp. 1\u201315, 1995."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784740"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133878"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_11"},{"key":"e_1_2_2_13_1","first-page":"100","volume-title":"European Conference on Object-Oriented Programming","author":"Bierman Gavin","year":"2010","unstructured":"Gavin Bierman , Erik Meijer , and Mads Torgersen . Adding Dynamic Types to C# . European Conference on Object-Oriented Programming , pp. 76\u2013 100 , 2010 . Gavin Bierman, Erik Meijer, and Mads Torgersen. Adding Dynamic Types to C#. European Conference on Object-Oriented Programming, pp. 76\u2013100, 2010."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640098"},{"key":"e_1_2_2_15_1","first-page":"94","volume-title":"Sam Tobin-Hochstadt. Practical Optional Types for Clojure. European Symposium on Programming","author":"Bonnaire-Sergeant Ambrose","year":"2016","unstructured":"Ambrose Bonnaire-Sergeant , Rowan Davies , and Sam Tobin-Hochstadt. Practical Optional Types for Clojure. European Symposium on Programming , pp. 68\u2013 94 , 2016 . Ambrose Bonnaire-Sergeant, Rowan Davies, and Sam Tobin-Hochstadt. Practical Optional Types for Clojure. European Symposium on Programming, pp. 68\u201394, 2016."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/165854.165893"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384659"},{"key":"e_1_2_2_18_1","first-page":"23","volume-title":"Jan Vitek. KafKa: Gradual Typing for Objects. European Conference on Object-Oriented Programming","author":"Chung Benjamin W.","year":"2018","unstructured":"Benjamin W. Chung , Paley Li , Francesco Zappa Nardelli , and Jan Vitek. KafKa: Gradual Typing for Objects. European Conference on Object-Oriented Programming , pp. 12:1\u201312: 23 , 2018 . Benjamin W. Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek. KafKa: Gradual Typing for Objects. European Conference on Object-Oriented Programming, pp. 12:1\u201312:23, 2018."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103766"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2039346.2039348"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926410"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_11"},{"key":"e_1_2_2_24_1","first-page":"128","volume-title":"Anne Rogers. Lazy Contract Checking for Immutable Data Structures. International Symposium Functional and Logic Programming","author":"Findler Robert Bruce","year":"2007","unstructured":"Robert Bruce Findler , Shu-yu Guo, and Anne Rogers. Lazy Contract Checking for Immutable Data Structures. International Symposium Functional and Logic Programming , pp. 111\u2013 128 , 2007 . Robert Bruce Findler, Shu-yu Guo, and Anne Rogers. Lazy Contract Checking for Immutable Data Structures. International Symposium Functional and Logic Programming, pp. 111\u2013128, 2007."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231387"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529700"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094830"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676967"},{"key":"e_1_2_2_30_1","volume-title":"A Spectrum of Type Soundness and Performance Supplementary Material","author":"Greenman Ben","year":"2018","unstructured":"Ben Greenman and Matthias Felleisen . A Spectrum of Type Soundness and Performance Supplementary Material . Northeastern University , NU-CCIS- 2018 -002, 2018. Ben Greenman and Matthias Felleisen. A Spectrum of Type Soundness and Performance Supplementary Material. Northeastern University, NU-CCIS-2018-002, 2018."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3162066"},{"key":"e_1_2_2_32_1","volume-title":"Jan Vitek, and Matthias Felleisen. How to Evaluate the Performance of Gradual Type Systems. Submitted for publication","author":"Greenman Ben","year":"2016","unstructured":"Ben Greenman , Asumu Takikawa , Max S. New , Daniel Feltey , Robert Bruce Findler , Jan Vitek, and Matthias Felleisen. How to Evaluate the Performance of Gradual Type Systems. Submitted for publication , 2016 . Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, Robert Bruce Findler, Jan Vitek, and Matthias Felleisen. How to Evaluate the Performance of Gradual Type Systems. Submitted for publication, 2016."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/182409.182495"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2989225.2989226"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224203"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110284"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_2_2_41_1","first-page":"426","volume-title":"Leroy and Michael Mauny. Dynamics in ML. International Conference on Functional Programming Languages and Computer Architecture","author":"Xavier","year":"1991","unstructured":"Xavier Leroy and Michael Mauny. Dynamics in ML. International Conference on Functional Programming Languages and Computer Architecture , pp. 406\u2013 426 , 1991 . Xavier Leroy and Michael Mauny. Dynamics in ML. International Conference on Functional Programming Languages and Computer Architecture, pp. 406\u2013426, 1991."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2816707.2816709"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2617548.2617553"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/258948.258962"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498930"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111057"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-005-4876-5"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_49_1","first-page":"0","article-title":"MACLISP Reference Manual. MIT","author":"Moon David A.","year":"1974","unstructured":"David A. Moon . MACLISP Reference Manual. MIT , Revision 0 , 1974 . David A. Moon. MACLISP Reference Manual. MIT, Revision 0, 1974.","journal-title":"Revision"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133880"},{"key":"e_1_2_2_51_1","volume-title":"New and Daniel R. Licata. Call-by-name Gradual Type Theory. International Conference on Formal Structures for Computation and Deduction","author":"Max","year":"2018","unstructured":"Max S. New and Daniel R. Licata. Call-by-name Gradual Type Theory. International Conference on Formal Structures for Computation and Deduction , 2018 . Max S. New and Daniel R. Licata. Call-by-name Gradual Type Theory. International Conference on Formal Structures for Computation and Deduction, 2018."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158529"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640134.1640145"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384592.2384599"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000219"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103714"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676971"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480362.2480655"},{"key":"e_1_2_2_59_1","first-page":"523","volume-title":"Information Processing","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds . Types, Abstraction, and Parametric Polymorphism . Information Processing , pp. 513\u2013 523 , 1983 . John C. Reynolds. Types, Abstraction, and Parametric Polymorphism. Information Processing, pp. 513\u2013523, 1983."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133879"},{"key":"e_1_2_2_61_1","first-page":"100","volume-title":"Jan Vitek. Concrete Types for TypeScript. European Conference on ObjectOriented Programming","author":"Richards Gregor","year":"2015","unstructured":"Gregor Richards , Zappa Nardelli , Francesco, and Jan Vitek. Concrete Types for TypeScript. European Conference on ObjectOriented Programming , pp. 76\u2013 100 , 2015 . Gregor Richards, Zappa Nardelli, Francesco, and Jan Vitek. Concrete Types for TypeScript. European Conference on ObjectOriented Programming, pp. 76\u2013100, 2015."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737968"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_2"},{"key":"e_1_2_2_65_1","volume-title":"Siek and Walid Taha. Gradual Typing for Functional Languages. Scheme and Functional Programming","author":"Jeremy","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha. Gradual Typing for Functional Languages. Scheme and Functional Programming . University of Chicago , TR- 2006 -06, 2006. Jeremy G. Siek and Walid Taha. Gradual Typing for Functional Languages. Scheme and Functional Programming. University of Chicago, TR-2006-06, 2006."},{"key":"e_1_2_2_66_1","first-page":"293","volume-title":"Refined Criteria for Gradual Typing. Summit oN Advances in Programming Languages","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek , Michael M. Vitousek , Matteo Cimini , and John Tang Boyland . Refined Criteria for Gradual Typing. Summit oN Advances in Programming Languages , pp. 274\u2013 293 , 2015 . Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined Criteria for Gradual Typing. Summit oN Advances in Programming Languages, pp. 274\u2013293, 2015."},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384629"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27694-1_21"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/1098646"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384685"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/567532.567553"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596598"},{"key":"e_1_2_2_74_1","first-page":"27","volume-title":"Matthias Felleisen. Towards Practical Gradual Typing. European Conference on Object-Oriented Programming","author":"Takikawa Asumu","year":"2015","unstructured":"Asumu Takikawa , Daniel Feltey , Earl Dean , Robert Bruce Findler , Matthew Flatt , Sam Tobin-Hochstadt , and Matthias Felleisen. Towards Practical Gradual Typing. European Conference on Object-Oriented Programming , pp. 4\u2013 27 , 2015 . Asumu Takikawa, Daniel Feltey, Earl Dean, Robert Bruce Findler, Matthew Flatt, Sam Tobin-Hochstadt, and Matthias Felleisen. Towards Practical Gradual Typing. European Conference on Object-Oriented Programming, pp. 4\u201327, 2015."},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837630"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384674"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96747"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863561"},{"key":"e_1_2_2_81_1","first-page":"17","volume-title":"Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. Migratory Typing: Ten years later. Summit oN Advances in Programming Languages","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. Migratory Typing: Ten years later. Summit oN Advances in Programming Languages , pp. 17:1\u201317: 17 , 2017 . Sam Tobin-Hochstadt, Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. Migratory Typing: Ten years later. Summit oN Advances in Programming Languages, pp. 17:1\u201317:17, 2017."},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661088.2661101"},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009849"},{"key":"e_1_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_2_85_1","first-page":"29","volume-title":"Jakub Zalewski. Mixed Messages: Measuring Conformance and NonInterference in TypeScript. European Conference on Object-Oriented Programming","author":"Williams Jack","year":"2017","unstructured":"Jack Williams , J. Garrett Morris , Philip Wadler , and Jakub Zalewski. Mixed Messages: Measuring Conformance and NonInterference in TypeScript. European Conference on Object-Oriented Programming , pp. 28:1\u201328: 29 , 2017 . Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. Mixed Messages: Measuring Conformance and NonInterference in TypeScript. European Conference on Object-Oriented Programming, pp. 28:1\u201328:29, 2017."},{"key":"e_1_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/239912.239917"},{"key":"e_1_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706343"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236766","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236766","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236766","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236766"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":88,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236766"],"URL":"https:\/\/doi.org\/10.1145\/3236766","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}