We consider the problem of specifying combinations of data structures with complex sharing in a manner that is declarative and results in provably correct code.Peter Hawkins, Martin Rinard, Alex Aiken, Mooly Sagiv, Kathleen Fisher From Communications of the ACM | December 2012