SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 14:00 - 14:20 at SPLASH-I - T-4 Chair(s): Michael Pradel, Sophia Drossopoulou
Wed 18 Nov 2020 02:00 - 02:20 at SPLASH-I - T-4 Chair(s): Sophia Drossopoulou, Julien Lange

Every newly created object goes through several initialization states:
starting from a state where all fields are uninitialized until all of
them are assigned. Any operation on the object during its initialization
process, which usually happens in the constructor via \emph{this}, has to
observe the initialization states of the object for correctness,
i.e.~only initialized fields may be used. Checking safe usage of
\emph{this} statically, without manual annotation of initialization
states in the source code, is a challenge, due to aliasing and virtual method
calls on \emph{this}.

Mainstream languages either do not check initialization errors, such as
Java, C++, Scala, or they defend against them by not supporting useful
initialization patterns, such as Swift. In parallel, past research has
shown that safe initialization can be achieved for varying degrees of
expressiveness but by sacrificing syntactic simplicity.

We approach the problem by upholding \emph{local reasoning about
initialization} which avoids whole-program analysis, and we achieve
\emph{typestate polymorphism} via subtyping.
On this basis, we put forward a
novel type-and-effect system that can effectively ensure
initialization safety while allowing flexible initialization patterns.
We implement an initialization checker in the Scala 3 compiler and
evaluate on several real-world projects.

Tue 17 Nov

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

Wed 18 Nov

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