The Scala programming language makes \emph{all} reference types \emph{implicitly nullable}. This is a problem, because null references do not support most operations that do make sense on regular objects, leading to runtime errors. In this paper, we present a modification to the Scala type system that makes nullability \emph{explicit} in the types. Specifically, we make reference types \emph{non-nullable} by default, while still allowing for nullable types via \emph{union types}. We have implemented this design for explicit nulls as a fork of the Dotty (Scala 3) compiler. We evaluate our scheme by migrating a number of Scala libraries to use explicit nulls. Finally, we give a \emph{denotational semantics} of \emph{type nullification}, the interoperability layer between Java and Scala with explicit nulls. We show a soundness theorem stating that, for variants of System F that model Java and Scala, nullification (mostly) preserves elements of types.

The artifact consists of a VM containing a modified copy of the Dotty compiler, plus proofs of the theorems in the paper.