SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 12:00 - 12:20 at SPLASH-III - F-3B Chair(s): Francisco Ferreira, Yaniv David
Sat 21 Nov 2020 00:00 - 00:20 at SPLASH-III - F-3B Chair(s): Dimitri Racordon, Yulei Sui

The Dependent Object Types (DOT) calculus serves as a foundation of the Scala programming language, with a machine-verified soundness proof. However, Scala's type system has been shown to be unsound due to null references, which are used as default values of fields of objects before they have been initialized. This paper proposes ιDOT, an extension of DOT for ensuring safe initialization of objects. DOT was previously extended to κDOT with the addition of mutable fields and constructors. To κDOT, ιDOT adds an initialization effect system that statically prevents the possibility of reading a null reference from an uninitialized object. To design ιDOT, we have reformulated the Freedom Before Commitment object initialization scheme in terms of disjoint subheaps to make it easier to formalize in an effect system and prove sound. Soundness of ιDOT depends on the interplay of three systems of rules: a type system close to that of DOT, an effect system to ensure definite assignment of fields in each constructor, and an initialization system that tracks the initialization status of objects in a stack of subheaps. We have proven the overall system sound and verified the soundness proof using the Coq proof assistant.

Fri 20 Nov
Times are displayed in time zone: Central Time (US & Canada) change

11:00 - 12:20: F-3BOOPSLA at SPLASH-III +12h
Chair(s): Francisco FerreiraImperial College London, Yaniv DavidTechnion
11:00 - 11:20
Talk
OOPSLA
Shraddha BarkeUniversity of California at San Diego, Hila PelegUniversity of California at San Diego, Nadia PolikarpovaUniversity of California at San Diego
Link to publication DOI Media Attached
11:20 - 11:40
Talk
OOPSLA
John Peter CamporaUniversity of Louisiana at Lafayette, Sheng ChenUniversity of Louisiana at Lafayette
Link to publication DOI Media Attached
11:40 - 12:00
Talk
OOPSLA
Yu WangNanjing University, Ke WangVisa Research, Fengjuan GaoNanjing University, Linzhang WangNanjing University
Link to publication DOI Media Attached
12:00 - 12:20
Talk
OOPSLA
Ifaz KabirUniversity of Alberta, Yufeng LiUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
Link to publication DOI Media Attached
23:00 - 00:20: F-3BOOPSLA at SPLASH-III
Chair(s): Dimitri RacordonUniversity of Geneva, Switzerland, Yulei SuiUniversity of Technology Sydney
23:00 - 23:20
Talk
OOPSLA
Shraddha BarkeUniversity of California at San Diego, Hila PelegUniversity of California at San Diego, Nadia PolikarpovaUniversity of California at San Diego
Link to publication DOI Media Attached
23:20 - 23:40
Talk
OOPSLA
John Peter CamporaUniversity of Louisiana at Lafayette, Sheng ChenUniversity of Louisiana at Lafayette
Link to publication DOI Media Attached
23:40 - 00:00
Talk
OOPSLA
Yu WangNanjing University, Ke WangVisa Research, Fengjuan GaoNanjing University, Linzhang WangNanjing University
Link to publication DOI Media Attached
00:00 - 00:20
Talk
OOPSLA
Ifaz KabirUniversity of Alberta, Yufeng LiUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
Link to publication DOI Media Attached