Peter Müller

"Alias Control with Universe Types: Overview and Challenges"

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 and explain how it enables modular verification of object invariants. I will also discuss open challenges for ownership type systems and propose solutions.