ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Sun 15 Nov 2020 09:40 - 10:00 at SPLASH-I - S-2 Chair(s): Shigeru Chiba, Yu David Liu
Sun 15 Nov 2020 21:40 - 22:00 at SPLASH-I - S-2 Chair(s): Atsushi Igarashi, Hidehiko Masuhara

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 LambdaNull, 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 LambdaNull, we then define a second calculus, StratifiedLambdaNull, 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 StratifiedLambdaNull 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.

Sun 15 Nov

Displayed time zone: Central Time (US & Canada) change

09:00 - 10:20
S-2Research Papers at SPLASH-I +12h
Chair(s): Shigeru Chiba The University of Tokyo, Yu David Liu State University of New York (SUNY) Binghamton
09:00
20m
Talk
Abstracting gradual referencesSCICO Journal-First
Research Papers
Matías Toro University of Chile, Éric Tanter University of Chile
Link to publication DOI Media Attached
09:20
20m
Talk
Don't Panic! Better, Fewer, Syntax Errors for LR Parsers
Research Papers
Lukas Diekmann King's College London, Laurence Tratt King's College London
Link to publication DOI Pre-print Media Attached
09:40
20m
Talk
Blame for Null
Research Papers
Abel Nieto Aarhus University, Marianna Rapoport University of Waterloo, Gregor Richards University of Waterloo, Ondřej Lhoták University of Waterloo
Link to publication DOI Pre-print Media Attached
10:00
20m
Talk
Perfect is the Enemy of Good: Best-Effort Program Synthesis
Research Papers
Hila Peleg University of California at San Diego, Nadia Polikarpova University of California at San Diego
Link to publication DOI Media Attached
21:00 - 22:20
S-2Research Papers at SPLASH-I
Chair(s): Atsushi Igarashi Kyoto University, Japan, Hidehiko Masuhara Tokyo Institute of Technology
21:00
20m
Talk
Abstracting gradual referencesSCICO Journal-First
Research Papers
Matías Toro University of Chile, Éric Tanter University of Chile
Link to publication DOI Media Attached
21:20
20m
Talk
Don't Panic! Better, Fewer, Syntax Errors for LR Parsers
Research Papers
Lukas Diekmann King's College London, Laurence Tratt King's College London
Link to publication DOI Pre-print Media Attached
21:40
20m
Talk
Blame for Null
Research Papers
Abel Nieto Aarhus University, Marianna Rapoport University of Waterloo, Gregor Richards University of Waterloo, Ondřej Lhoták University of Waterloo
Link to publication DOI Pre-print Media Attached
22:00
20m
Talk
Perfect is the Enemy of Good: Best-Effort Program Synthesis
Research Papers
Hila Peleg University of California at San Diego, Nadia Polikarpova University of California at San Diego
Link to publication DOI Media Attached