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: https://drops.dagstuhl.de/opus/volltexte/2020/13207/
Nieto, Abel ; Rapoport, Marianna ; Richards, Gregor ; Lhoták, Ondřej
Blame for Null (Artifact)
| pdf-format: |
|
|
| artifact-format: |
|
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 | |
| Seminar: | 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 |
