4 Search Results for "Rapoport, Marianna"

Issue

DARTS, Volume 4, Issue 3

Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Editors: Maria Christakis, Philipp Haller, Marianna Rapoport, and Marianna Rapoport

Document
Artifact
DOI: 10.4230/DARTS.6.2.10
Blame for Null (Artifact)

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

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

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.
Cite as

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)

Copy BibTex To Clipboard

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

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

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Multiple modern programming languages, including Kotlin, Scala, Swift, and C#, have type systems where nullability is explicitly specified in the types. All of the above also need to interoperate with languages where types remain implicitly nullable, like Java. This leads to runtime errors that can manifest in subtle ways. In this paper, we show how to reason about the presence and provenance of such nullability errors using the concept of blame from gradual typing. Specifically, we introduce a calculus, λ_null, where some terms are typed as implicitly nullable and others as explicitly nullable. Just like in the original blame calculus of Wadler and Findler, interactions between both kinds of terms are mediated by casts with attached blame labels, which indicate the origin of errors. On top of λ_null, we then create a second calculus, λ_null^s, which closely models the interoperability between languages with implicit nullability and languages with explicit nullability, such as Java and Scala. Our main result is a theorem that states that nullability errors in λ_null^s can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. By analogy, this would mean that NullPointerExceptions in combined Java/Scala programs are always the result of unsoundness in the Java type system. We summarize our result with the slogan explicitly nullable programs can't be blamed. All our results are formalized in the Coq proof assistant.
Cite as

Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. Blame for Null. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 3:1-3:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{nieto_et_al:LIPIcs.ECOOP.2020.3,
  author =	{Nieto, Abel and Rapoport, Marianna and Richards, Gregor and Lhot\'{a}k, Ond\v{r}ej},
  title =	{{Blame for Null}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{3:1--3:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.3},
  URN =		{urn:nbn:de:0030-drops-131606},
  doi =		{10.4230/LIPIcs.ECOOP.2020.3},
  annote =	{Keywords: nullability, type systems, blame calculus, gradual typing}
}
Document
DOI: 10.4230/DARTS.4.3.0
Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee

Authors: Maria Christakis, Philipp Haller, Marianna Rapoport, and Marianna Rapoport

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Cite as

Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{christakis_et_al:DARTS.4.3.0,
  author =	{Christakis, Maria and Haller, Philipp and Rapoport, Marianna and Rapoport, Marianna},
  title =	{{Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}},
  pages =	{0:i--0:xii},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Christakis, Maria and Haller, Philipp and Rapoport, Marianna and Rapoport, Marianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.4.3.0},
  URN =		{urn:nbn:de:0030-drops-92327},
  doi =		{10.4230/DARTS.4.3.0},
  annote =	{Keywords: Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}
}
  • Refine by Author
  • 3 Rapoport, Marianna
  • 2 Lhoták, Ondřej
  • 2 Nieto, Abel
  • 2 Richards, Gregor
  • 1 Christakis, Maria
  • Show More...

  • Refine by Classification
  • 2 Software and its engineering → General programming languages
  • 2 Software and its engineering → Interoperability
  • 2 Theory of computation → Operational semantics
  • 2 Theory of computation → Type theory

  • Refine by Keyword
  • 2 blame calculus
  • 2 gradual typing
  • 2 nullability
  • 2 type systems
  • 1 Artifact Evaluation Committee
  • Show More...

  • Refine by Type
  • 3 document
  • 1 issue

  • Refine by Publication Year
  • 2 2018
  • 2 2020

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