Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online

Imperative object-oriented languages usually allow multiple references to the same object to co- exist. This aliasing is a powerful tool necessary to express complex data structures and to manipulate those. Unrestricted aliasing however, as found in Java for example, complicates reasoning about programs’ behaviour. Any statement could, in principle, modify any object in the heap. Isolation has been developed, under one form or another, in many type systems as a way of restricting what references are allowed to co-exist. It has been leveraged, among others, to support security, garbage collection, data-race freedom. However by restricting what aliases can exist, these type systems necessarily reduce their expressivity. In some languages, such as Rust, the shape of the object graph cannot express cyclic data structures. In others, such as Pony and Midori, common access patterns and algorithms on data structures cannot be implemented, short of jumping through many hoops. Our work attempts to develop a system that improves on previous languages, making them more expressive without compromising safety. We allow arbitrary heap topologies and data structures to be represented while supporting advanced manipulation of them.