{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:47Z","timestamp":1779836747400,"version":"3.53.1"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2024,12,27]],"date-time":"2024-12-27T00:00:00Z","timestamp":1735257600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Gradual typing provides a model for when a legacy language with less precise types interacts with a newer language with more precise types. Casts mediate between types of different precision, allocating blame when a value fails to conform to a type. The blame theorem asserts that blame always falls on the less-precisely typed side of a cast. One instance of interest is when a legacy language (such as Java) permits null values at every type, while a newer language (such as Scala or Kotlin) explicitly indicates which types permit null values. Nieto et al. in 2020 introduced a gradually typed calculus for just this purpose. The calculus requires three distinct constructors for function types and a non-standard proof of the blame theorem; it can embed terms from the legacy language into the newer language (or vice versa) only when they are closed. Here, we define a simpler calculus that is more orthogonal, with one constructor for function types and one for possibly nullable types, and with an entirely standard proof of the blame theorem; it can embed terms from the legacy language into the newer language (and vice versa) even if they are open. All results in the paper have been mechanized in Coq.<\/jats:p>","DOI":"10.1017\/s0956796824000121","type":"journal-article","created":{"date-parts":[[2024,12,26]],"date-time":"2024-12-26T22:43:17Z","timestamp":1735252997000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["A simple blame calculus for explicit nulls"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9066-1889","authenticated-orcid":false,"given":"OND\u0158EJ","family":"LHOT\u00c1K","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7619-6378","authenticated-orcid":false,"given":"PHILIP","family":"WADLER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2024,12,27]]},"reference":[{"key":"S0956796824000121_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"S0956796824000121_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268961"},{"key":"S0956796824000121_ref27","unstructured":"Siek, J. G. , Vitousek, M. M. , Cimini, M. & Boyland, J. T. (2015) Refined criteria for gradual typing. In 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA (LIPIcs, Vol. 32), Ball, T. , Bod\u00edk, R. , Krishnamurthi, S. , Lerner, B. S. & Morrisett, G. (eds.), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 274\u2013293."},{"key":"S0956796824000121_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"S0956796824000121_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053388"},{"key":"S0956796824000121_ref15","unstructured":"JetBrains (2022) Kotlin Programming Language. https:\/\/kotlinlang.org\/ (accessed 17 March 2022)."},{"key":"S0956796824000121_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984004"},{"key":"S0956796824000121_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268960"},{"key":"S0956796824000121_ref23","unstructured":"Patrignani, M. (2021) Why Should Anyone use Colours? or, Syntax Highlighting Beyond Code Snippets. [arxiv]2001.11334 [cs.SE]"},{"key":"S0956796824000121_ref30","unstructured":"Tufte, E. R. (2001) The Visual Display of Quantitative Information (second ed.). Graphics Press, Cheshire, Connecticut."},{"key":"S0956796824000121_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190220"},{"key":"S0956796824000121_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3485503"},{"key":"S0956796824000121_ref25","unstructured":"Siek, J. G. & Taha, W. (2006) Gradual typing for functional languages. In Scheme and Functional Programming Workshop, Vol. 6, pp. 81\u201392."},{"key":"S0956796824000121_ref8","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2021.3"},{"key":"S0956796824000121_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"S0956796824000121_ref19","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.3"},{"key":"S0956796824000121_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"S0956796824000121_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"S0956796824000121_ref3","unstructured":"Apple (2022) The Swift Programming Language. https:\/\/docs.swift.org\/swift-book\/ (accessed 17 March 2022)."},{"key":"S0956796824000121_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"S0956796824000121_ref13","unstructured":"Hoare, T. (2009) Null References: The Billion Dollar Mistake. https:\/\/www.infoq.com\/presentations\/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare\/ (accessed 17 March 2022)."},{"key":"S0956796824000121_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"S0956796824000121_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"S0956796824000121_ref20","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.25"},{"key":"S0956796824000121_ref33","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796824000121_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3428217"},{"key":"S0956796824000121_ref31","unstructured":"Wadler, P. (2015) A complement to blame. In 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA (LIPIcs, Vol. 32), Ball, T. , Bod\u00edk, R. , Krishnamurthi, S. , Lerner, B. S. & Morrisett, G. (eds.), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 309\u2013320."},{"key":"S0956796824000121_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48737-9_3"},{"key":"S0956796824000121_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"S0956796824000121_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"S0956796824000121_ref4","volume-title":"Computer and Information Science","author":"Aydemir","year":"2010"},{"key":"S0956796824000121_ref18","unstructured":"Microsoft (2022) C# Language Specification. https:\/\/docs.microsoft.com\/en-us\/dotnet\/csharp\/language-reference\/language-specification (accessed 17 March 2022)."},{"key":"S0956796824000121_ref21","first-page":"1","article-title":"Scala with explicit nulls (artifact)","volume":"6","author":"Nieto","year":"2020","journal-title":"Dagstuhl Artifacts Ser."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796824000121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:34Z","timestamp":1779834994000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796824000121\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,27]]},"references-count":33,"alternative-id":["S0956796824000121"],"URL":"https:\/\/doi.org\/10.1017\/s0956796824000121","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,27]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e15"}}