Blame for Null (Artifact)

Authors Abel Nieto , Marianna Rapoport, Gregor Richards , Ondřej Lhoták

Thumbnail PDF

Artifact Description

  • Filesize: 291 kB
  • 2 pages

Document Identifiers

Author Details

Abel Nieto
  • University of Waterloo, Canada
Marianna Rapoport
  • University of Waterloo, Canada
Gregor Richards
  • University of Waterloo, Canada
Ondřej Lhoták
  • University of Waterloo, Canada


We would like to thank the anonymous reviewers for their valuable feedback.

Cite AsGet BibTex

Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. Blame for Null (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)



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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
  • Theory of computation → Type theory
  • Software and its engineering → Interoperability
  • Theory of computation → Operational semantics
  • nullability
  • type systems
  • blame calculus
  • gradual typing


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads