Weak Updates and Separation Logic

Separation logic provides a simple but powerful technique for reasoning about low-level imperative programs that use shared data structures. Unfortunately, separation logic supports only "Strong updates", in which mutation to a heap location is safe only if a unique reference is owned. This limits the applicability of separation logic when reasoning about the interaction between many high-level languages (e.g., ML, Java, C#) and low-level ones since the high-level languages do not support strong updates. Instead, they adopt the discipline of "Weak updates", in which there is a global "Heap type" to enforce the invariant of type-preserving heap updates.