A conceptual framework for safe object initialization: a principled and mechani...
summary
Defines four enforceable principles—monotonicity, authority, stackability, scopability—and builds a small Celsius calculus that encodes temperature-annotated types and mandatory field initializers to prevent early field access. Provides a mechanized soundness proof in Coq and a practical Scala implementation (compiler option available) showing local reasoning: code running in a hot context produces only fully initialized objects. Explains which cyclic initialization patterns are allowed and which are statically rejected.
AI-written summary · about
chapters (10)
- 0:00Safe object initialization intro
- 2:51Initialization design challenges
- 4:13Celsius model requirements
- 5:36Celsius model principles
- 6:42Monotonicity and authority
- 9:08Stackability and scalability
- 11:55Local reasoning and typing
- 13:41Temperature annotations in Scala
- 14:46Takeaways and insights
- 15:28Q&A
related talks
15mModular Reasoning about Global Variables and Their Initialization
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
15mIncremental Certified Programming
51mFunctional Principles for Object Oriented Development
34mHow I learned to stop worrying and love Functional Design
01h 00mThe Nightmare of Initialization in C++
17mReasoning about External Calls
21mMechanised Hypersafety Proofs about Structured Data