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): Yaniv David, Francisco Ferreira
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

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

11:00 - 12:20
F-3BOOPSLA at SPLASH-III +12h
Chair(s): Yaniv David Technion, Francisco Ferreira Imperial College London
11:00
20m
Talk
Just-in-Time Learning for Bottom-Up Enumerative Synthesis
OOPSLA
Shraddha Barke University of California at San Diego, Hila Peleg University of California at San Diego, Nadia Polikarpova University of California at San Diego
Link to publication DOI Media Attached
11:20
20m
Talk
Taming Type Annotations in Gradual Typing
OOPSLA
John Peter Campora University of Louisiana at Lafayette, Sheng Chen University of Louisiana at Lafayette
Link to publication DOI Media Attached
11:40
20m
Talk
Learning Semantic Program Embeddings with Graph Interval Neural NetworkDistinguished Paper
OOPSLA
Yu Wang Nanjing University, Ke Wang Visa Research, Fengjuan Gao Nanjing University, Linzhang Wang Nanjing University
Link to publication DOI Media Attached
12:00
20m
Talk
ιDOT: A DOT Calculus with Object Initialization
OOPSLA
Ifaz Kabir University of Alberta, Yufeng Li University of Waterloo, Ondřej Lhoták University of Waterloo
Link to publication DOI Media Attached
23:00 - 00:20
F-3BOOPSLA at SPLASH-III
Chair(s): Dimitri Racordon University of Geneva, Switzerland, Yulei Sui University of Technology Sydney
23:00
20m
Talk
Just-in-Time Learning for Bottom-Up Enumerative Synthesis
OOPSLA
Shraddha Barke University of California at San Diego, Hila Peleg University of California at San Diego, Nadia Polikarpova University of California at San Diego
Link to publication DOI Media Attached
23:20
20m
Talk
Taming Type Annotations in Gradual Typing
OOPSLA
John Peter Campora University of Louisiana at Lafayette, Sheng Chen University of Louisiana at Lafayette
Link to publication DOI Media Attached
23:40
20m
Talk
Learning Semantic Program Embeddings with Graph Interval Neural NetworkDistinguished Paper
OOPSLA
Yu Wang Nanjing University, Ke Wang Visa Research, Fengjuan Gao Nanjing University, Linzhang Wang Nanjing University
Link to publication DOI Media Attached
00:00
20m
Talk
ιDOT: A DOT Calculus with Object Initialization
OOPSLA
Ifaz Kabir University of Alberta, Yufeng Li University of Waterloo, Ondřej Lhoták University of Waterloo
Link to publication DOI Media Attached