Document Open Access Logo

Blame for Null (Artifact)

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

PDF
Thumbnail PDF

Artifact Description

DARTS.6.2.10.pdf
  • 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

Funding

This research was supported by the Natural Sciences and Engineering Research Council of Canada and by the Waterloo-Huawei Joint Innovation Lab.

Acknowledgements

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)
https://doi.org/10.4230/DARTS.6.2.10

Artifact

Abstract

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
Keywords
  • nullability
  • type systems
  • blame calculus
  • gradual typing

Metrics

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

Related Article

  • Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták, "Blame for Null", in 34th European Conference on Object-Oriented Programming (ECOOP 2020), LIPIcs, Vol. 166, pp. 3:1 - 3:28, 2020. https://doi.org/10.4230/LIPIcs.ECOOP.2020.3
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact