2026-07-22T22:18:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13207 2024-03-06T11:05:09Z ddc:004 open_access

Blame for Null (Artifact) Nieto, Abel Rapoport, Marianna Richards, Gregor Lhoták, Ondřej nullability type systems blame calculus gradual typing This artifact is a companion to the paper "Blame for Null", where we formalize multiple calculi to reason about the interoperability between languages where nullability is explicit and those where nullability is implicit. Our main result is a theorem that states that nullability errors can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. We summarize our result with the slogan explicitly nullable programs can't be blamed. The artifact consists of a mechanized Coq proof of the results presented in the paper. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Abel Nieto and Marianna Rapoport and Gregor Richards and Ondřej Lhoták 2020 Is Part Of DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.6.2.10 urn:nbn:de:0030-drops-132070 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.10 eng https://creativecommons.org/licenses/by/3.0/legalcode