{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:29Z","timestamp":1750220669709,"version":"3.41.0"},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>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 \u03b9DOT, an extension of DOT for ensuring safe initialization of objects. DOT was previously extended to \u03baDOT with the addition of mutable fields and constructors. To \u03baDOT, \u03b9DOT adds an initialization effect system that statically prevents the possibility of reading a null reference from an uninitialized object. To design \u03b9DOT, 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 \u03b9DOT 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.<\/jats:p>","DOI":"10.1145\/3428276","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["\u03b9DOT: a DOT calculus with object initialization"],"prefix":"10.1145","volume":"4","author":[{"given":"Ifaz","family":"Kabir","sequence":"first","affiliation":[{"name":"University of Alberta, Canada"}]},{"given":"Yufeng","family":"Li","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}]},{"given":"Ond\u0159ej","family":"Lhot\u00e1k","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660216"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984004"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297052"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41654"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_24"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3241653.3241659"},{"volume-title":"DOT: A DOT Calculus with Object Initialization. Technical Report CS-2020-06","year":"2020","author":"Kabir Ifaz","key":"e_1_2_2_8_1"},{"key":"e_1_2_2_9_1","unstructured":"Martin Odersky Philippe Altherr Vincent Cremet Iulian Dragos Gilles Dubochet Burak Emir Sean McDirmid St\u00e9phane Micheloud Nikolay Mihaylov Michel Schinz Lex Spoon Erik Stenman and Matthias Zenger. 2006. An Overview of the Scala Programming Language (2. Edition). ( 2006 ). http:\/\/infoscience.epfl.ch\/record\/ 85634  Martin Odersky Philippe Altherr Vincent Cremet Iulian Dragos Gilles Dubochet Burak Emir Sean McDirmid St\u00e9phane Micheloud Nikolay Mihaylov Michel Schinz Lex Spoon Erik Stenman and Matthias Zenger. 2006. An Overview of the Scala Programming Language (2. Edition). ( 2006 ). http:\/\/infoscience.epfl.ch\/record\/ 85634"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480890"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133870"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360571"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_9"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002712"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048142"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428276","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428276","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428276"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":17,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428276"],"URL":"https:\/\/doi.org\/10.1145\/3428276","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}