The ownerships of ConSORT also have
a connection to separation logic [1]};
the separating conjunction isolates write effects to local subheaps,
while ConSORT's ownership system isolates effects to local updates of pointer types.
Other researchers have used separation logic to precisely
support strong updates of abstract state.
For example, in work by Kloos et al. [2]}
resources are associated with static, abstract names; each
resource (represented by its static name) may be owned (and thus,
mutated) by exactly one thread. Unlike ConSORT, their ownership
system forbids even temporary immutable,
shared ownership, or transferring ownerships at arbitrary program points.
An approach proposed by Bakst and Jhala [3]}
uses a similar technique,
combining separation logic with refinement types. Their approach gives
allocated memory cells abstract names, and associates these names with
refinements in an abstract heap. Like the approach of Kloos et al.
and ConSORT's ownership 1 pointers, they
ensure these abstract locations are distinct
in all concrete heaps, enabling sound, strong updates.
