{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:07:35Z","timestamp":1760044055516,"version":"3.41.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K034413\/1"],"award-info":[{"award-number":["EP\/K034413\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006112","name":"Microsoft Research","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006112","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,10,24]]},"abstract":"<jats:p>Gradual typing has emerged as the tonic for programmers with a thirst for a blend of static and dynamic typing. Contracts provide a lightweight form of gradual typing as they can be implemented as a library, rather than requiring a gradual type system.<\/jats:p>\n          <jats:p>Intersection and union types are well suited to static and dynamic languages: intersection encodes overloaded functions; union encodes uncertain data arising from branching code. We extend the untyped lambda calculus with contracts for monitoring higher-order intersection and union types, for the first time giving a uniform treatment to both. Each operator requires a single reduction rule that does not depend on the constituent types or the context of the operator.<\/jats:p>\n          <jats:p>We present a new method for defining contract satisfaction based on blame behaviour. A value positively satisfies a type if applying a contract of that type can never elicit positive blame. A continuation negatively satisfies a type if applying a contract of that type can never elicit negative blame. We supplement our definition of satisfaction with a series of monitoring properties that satisfying values and continuations should have.<\/jats:p>","DOI":"10.1145\/3276504","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["The root cause of blame: contracts for intersection and union types"],"prefix":"10.1145","volume":"2","author":[{"given":"Jack","family":"Williams","sequence":"first","affiliation":[{"name":"University of Edinburgh, UK"}]},{"given":"J. Garrett","family":"Morris","sequence":"additional","affiliation":[{"name":"University of Kansas, USA"}]},{"given":"Philip","family":"Wadler","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"With and Without Types. In ACM International Conference on Functional Programming (ICFP).","author":"Ahmed Amal","year":"2017","unstructured":"Amal Ahmed , Dustin Jamner , Jeremy G. Siek , and Philip Wadler . 2017 . Theorems for Free for Free: Parametricity , With and Without Types. In ACM International Conference on Functional Programming (ICFP). Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free: Parametricity, With and Without Types. In ACM International Conference on Functional Programming (ICFP)."},{"volume-title":"Theoretical Aspects of Computer Software, Takayasu Ito and Albert R","author":"Barbanera Franco","key":"e_1_2_2_2_1","unstructured":"Franco Barbanera and Mariangiola Dezani-Ciancaglini . 1991. Intersection and Union Types . In Theoretical Aspects of Computer Software, Takayasu Ito and Albert R . Meyer (Eds.). Springer Berlin Heidelberg . Franco Barbanera and Mariangiola Dezani-Ciancaglini. 1991. Intersection and Union Types. In Theoretical Aspects of Computer Software, Takayasu Ito and Albert R. Meyer (Eds.). Springer Berlin Heidelberg."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_11"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005971"},{"key":"e_1_2_2_5_1","volume-title":"Gradual Typing with Union and Intersection Types. In ACM International Conference on Functional Programming (ICFP).","author":"Castagna Giuseppe","year":"2017","unstructured":"Giuseppe Castagna and Victor Lanvin . 2017 . Gradual Typing with Union and Intersection Types. In ACM International Conference on Functional Programming (ICFP). Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. In ACM International Conference on Functional Programming (ICFP)."},{"key":"e_1_2_2_6_1","volume-title":"Fast and Precise Type Checking for JavaScript. In ACM Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA).","author":"Chaudhuri Avik","year":"2017","unstructured":"Avik Chaudhuri , Panagiotis Vekris , Sam Goldman , Marshall Roch , and Gabriel Levi . 2017 . Fast and Precise Type Checking for JavaScript. In ACM Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA). Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, and Gabriel Levi. 2017. Fast and Precise Type Checking for JavaScript. In ACM Conference on Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA)."},{"key":"e_1_2_2_7_1","volume-title":"A new type assignment for \u03bb-terms. 19","author":"Coppo Mario","year":"1978","unstructured":"Mario Coppo and Mariangiola Dezani-Ciancaglini . 1978. A new type assignment for \u03bb-terms. 19 ( 1978 ), 139\u2013156. Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978. A new type assignment for \u03bb-terms. 19 (1978), 139\u2013156."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2039346.2039348"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926410"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_11"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Joshua Dunfield and Frank Pfenning. 2003. Type Assignment for Intersections and Unions in Call-by-Value Languages. In Foundations of Software Science and Computation Structures.   Joshua Dunfield and Frank Pfenning. 2003. Type Assignment for Intersections and Unions in Call-by-Value Languages. In Foundations of Software Science and Computation Structures.","DOI":"10.1007\/3-540-36576-1_16"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_16"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297081.1297089"},{"key":"e_1_2_2_18_1","volume-title":"Gradual Session Types. In ACM International Conference on Functional Programming (ICFP).","author":"Igarashi Atsushi","year":"2017","unstructured":"Atsushi Igarashi , Peter Thiemann , Vasco T. Vasconcelos , and Philip Wadler . 2017 b. Gradual Session Types. In ACM International Conference on Functional Programming (ICFP). Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler. 2017b. Gradual Session Types. In ACM International Conference on Functional Programming (ICFP)."},{"key":"e_1_2_2_19_1","volume-title":"On Polymorphic Gradual Typing. In ACM International Conference on Functional Programming (ICFP).","author":"Igarashi Yuu","year":"2017","unstructured":"Yuu Igarashi , Taro Sekiyama , and Atsushi Igarashi . 2017 a. On Polymorphic Gradual Typing. In ACM International Conference on Functional Programming (ICFP). Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017a. On Polymorphic Gradual Typing. In ACM International Conference on Functional Programming (ICFP)."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784737"},{"key":"e_1_2_2_21_1","volume-title":"TreatJS: Higher-Order Contracts for JavaScripts. In European Conference on Object-Oriented Programming (ECOOP) (Leibniz International Proceedings in Informatics (LIPIcs)). 28\u201351","author":"Keil Matthias","year":"2015","unstructured":"Matthias Keil and Peter Thiemann . 2015 b. TreatJS: Higher-Order Contracts for JavaScripts. In European Conference on Object-Oriented Programming (ECOOP) (Leibniz International Proceedings in Informatics (LIPIcs)). 28\u201351 . Matthias Keil and Peter Thiemann. 2015b. TreatJS: Higher-Order Contracts for JavaScripts. In European Conference on Object-Oriented Programming (ECOOP) (Leibniz International Proceedings in Informatics (LIPIcs)). 28\u201351."},{"volume-title":"Object-Oriented Software Construction","author":"Meyer Bertrand","key":"e_1_2_2_22_1","unstructured":"Bertrand Meyer . 1988. Object-Oriented Software Construction . Prentice-Hall, Inc. Bertrand Meyer. 1988. Object-Oriented Software Construction. Prentice-Hall, Inc."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/129093"},{"volume-title":"Typed Lambda Calculi and Applications","author":"Pierce Benjamin C.","key":"e_1_2_2_24_1","unstructured":"Benjamin C. Pierce . 1993. Intersection Types and Bounded Polymorphism . In Typed Lambda Calculi and Applications . Springer Berlin Heidelberg . Benjamin C. Pierce. 1993. Intersection Types and Bounded Polymorphism. In Typed Lambda Calculi and Applications. Springer Berlin Heidelberg."},{"volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme).","author":"Jeremy","key":"e_1_2_2_25_1","unstructured":"Jeremy G. Siek and Walid Taha. 2006 . Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme). Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme)."},{"key":"e_1_2_2_26_1","volume-title":"Siek and Sam Tobin-Hochstadt","author":"Jeremy","year":"2016","unstructured":"Jeremy G. Siek and Sam Tobin-Hochstadt . 2016 . The Recursive Union of Some Gradual Types. Springer International Publishing . Jeremy G. Siek and Sam Tobin-Hochstadt. 2016. The Recursive Union of Some Gradual Types. Springer International Publishing."},{"key":"e_1_2_2_27_1","volume-title":"Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)).","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek , Michael M. Vitousek , Matteo Cimini , and John Tang Boyland . 2015 a. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)). Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015a. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs))."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000047"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"Mat\u00edas Toro and \u00c9ric Tanter. 2017. A Gradual Interpretation of Union Types. In Static Analysis.  Mat\u00edas Toro and \u00c9ric Tanter. 2017. A Gradual Interpretation of Union Types. In Static Analysis.","DOI":"10.1007\/978-3-319-66706-5_19"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_29"},{"key":"e_1_2_2_33_1","unstructured":"Philip Wadler. 2015. A Complement to Blame. In SNAPL.  Philip Wadler. 2015. A Complement to Blame. In SNAPL."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_2_35_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\/3276504","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276504","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:03:39Z","timestamp":1750273419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276504"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":34,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276504"],"URL":"https:\/\/doi.org\/10.1145\/3276504","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}