License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.6.2.10
URN: urn:nbn:de:0030-drops-132070
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13207/
Go back to Dagstuhl Artifacts Series


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

Blame for Null (Artifact)

pdf-format:
DARTS-6-2-10.pdf (0.3 MB)


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.

BibTeX - Entry

@Article{nieto_et_al:DARTS:2020:13207,
  author =	{Abel Nieto and Marianna Rapoport and Gregor Richards and Ondřej Lhot{\'a}k},
  title =	{{Blame for Null (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13207},
  URN =		{urn:nbn:de:0030-drops-132070},
  doi =		{10.4230/DARTS.6.2.10},
  annote =	{Keywords: nullability, type systems, blame calculus, gradual typing}
}

Keywords: nullability, type systems, blame calculus, gradual typing
Collection: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Related Scholarly Article: https://doi.org/10.4230/LIPIcs.ECOOP.2020.3
Issue Date: 2020
Date of publication: 06.11.2020


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI