Events

In object-oriented programs, an object can potentially reference any other object in the heap and read and modify its fields. Such programs with arbitrary object structures are difficult to understand, to maintain, and to reason about. In this talk, I will present the Universe type system, which allows programmers to organize the heap into ownership contexts and to control modification of objects. I will give an overview of the Universe type system, explain how it enables modular verification of object invariants, and show how it solves the long-standing ownership transfer problem.