{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:16:19Z","timestamp":1784232979933,"version":"3.55.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"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":[[2022,10,31]]},"abstract":"<jats:p>An object under initialization does not fulfill its class specification yet and can be unsafe to  \n use as it may have uninitialized fields. It can sometimes be useful to call methods on such a  \n partially initialized object in order to compute a complex initial value, or to let the object  \n escape its constructor in order to create mutually recursive objects. However, inadvertent usage  \n of uninitialized fields can lead to run-time crashes. Those subtle programming errors are not  \n statically detected by most modern compilers.<\/jats:p>\n          <jats:p>While many other features of object-oriented programming languages have been thoroughly studied  \n over the years, object initialization lacks a simple, systematic, and principled  \n treatment. Building on the insights of previous work, we identify a set of four core principles  \n for safe initialization: monotonicity, authority, stackability, and scopability. We capture the  \n essence of the principles with a minimal calculus, Celsius, and show that the principles give rise  \n to a practical initialization system that strikes a balance between expressiveness and  \n simplicity. The meta-theory of the system is entirely mechanized using the Coq proof assistant. We  \n believe that our approach based on well-identified core principles sheds new light on the  \n underlying mechanisms ensuring safety and could serve as a basis for language design when faced  \n with similar challenges.<\/jats:p>","DOI":"10.1145\/3563314","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"729-757","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6333-6092","authenticated-orcid":false,"given":"Cl\u00e9ment","family":"Blaudeau","sequence":"first","affiliation":[{"name":"Inria, France \/ Universit\u00e9 de Paris-Cit\u00e9, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7949-4303","authenticated-orcid":false,"given":"Fengyun","family":"Liu","sequence":"additional","affiliation":[{"name":"Oracle Labs, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"A List of Successes That Can Change the World","author":"Amin Nada","unstructured":"Nada Amin , Samuel Gr\u00fctter , Martin Odersky , Tiark Rompf , and Sandro Stucki . 2016. The essence of dependent object types . In A List of Successes That Can Change the World . Springer , 249\u2013272. Nada Amin, Samuel Gr\u00fctter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The essence of dependent object types. In A List of Successes That Can Change the World. Springer, 249\u2013272."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. Pages: 666\u2013679 Publisher: ACM \t\t\t\t  Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. Pages: 666\u2013679 Publisher: ACM","DOI":"10.1145\/3093333.3009866"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7079830"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2008.7.5.a2"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048113"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Manuel F\u00e4hndrich and K. Rustan M. Leino. 2003. Declaring and checking non-null types in an object-oriented language. In OOPSLA. \t\t\t\t  Manuel F\u00e4hndrich and K. Rustan M. Leino. 2003. Declaring and checking non-null types in an object-oriented language. In OOPSLA.","DOI":"10.1145\/949305.949332"},{"key":"e_1_2_1_7_1","unstructured":"Manuel Fahndrich and Rustan Leino. 2003. Heap Monotonic Typestate. https:\/\/www.microsoft.com\/en-us\/research\/publication\/heap-monotonic-typestate\/ \t\t\t\t  Manuel Fahndrich and Rustan Leino. 2003. Heap Monotonic Typestate. https:\/\/www.microsoft.com\/en-us\/research\/publication\/heap-monotonic-typestate\/"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297052"},{"key":"e_1_2_1_9_1","unstructured":"James Gosling Bill Joy Guy Steele Gilad Bracha and Alex Buckley. 2015. The Java Language Specification Java SE 8 Edition. \t\t\t\t  James Gosling Bill Joy Guy Steele Gilad Bracha and Alex Buckley. 2015. The Java Language Specification Java SE 8 Edition."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-009-9042-z"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428276"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428243"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3486610.3486895"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Julian Mackay Hannes Mehnert Alex Potanin Lindsay J. Groves and Nicholas Robert Cameron. 2012. Encoding Featherweight Java with assignment and immutability using the Coq proof assistant. In FTfJP@ECOOP. \t\t\t\t  Julian Mackay Hannes Mehnert Alex Potanin Lindsay J. Groves and Nicholas Robert Cameron. 2012. Encoding Featherweight Java with assignment and immutability using the Coq proof assistant. In FTfJP@ECOOP.","DOI":"10.1145\/2318202.2318206"},{"key":"e_1_2_1_16_1","volume-title":"Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation","author":"Miller Mark Samuel","year":"2006","unstructured":"Mark Samuel Miller . 2006 . Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation . Johns Hopkins University . Baltimore, Maryland, USA. Mark Samuel Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation. Johns Hopkins University. Baltimore, Maryland, USA."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.25"},{"key":"e_1_2_1_18_1","unstructured":"Martin Odersky. 2019. Scala Language Specification. https:\/\/scala-lang.org\/files\/archive\/spec\/2.13\/ \t\t\t\t  Martin Odersky. 2019. Scala Language Specification. https:\/\/scala-lang.org\/files\/archive\/spec\/2.13\/"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328408.1328434"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480890"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434326"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Marco Servetto Julian Mackay Alex Potanin and James W Noble. 2013. The Billion-Dollar Fix - Safe Modular Circular Initialisation with Placeholders and Placeholder Types. In ECOOP. \t\t\t\t  Marco Servetto Julian Mackay Alex Potanin and James W Noble. 2013. The Billion-Dollar Fix - Safe Modular Circular Initialisation with Placeholders and Placeholder Types. In ECOOP.","DOI":"10.1007\/978-3-642-39038-8_9"},{"key":"e_1_2_1_24_1","volume-title":"Strom and Shaula Yemini","author":"Robert","year":"1986","unstructured":"Robert E. Strom and Shaula Yemini . 1986 . Typestate : A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, SE- 12 (1986), 157\u2013171. Robert E. Strom and Shaula Yemini. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, SE-12 (1986), 157\u2013171."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048142"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.038"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_10"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563314","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563314","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563314"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":27,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563314"],"URL":"https:\/\/doi.org\/10.1145\/3563314","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}