only one that is laid out neatly using the separating conjunction. This idea was taken much further by Yang, who used to provide localized reasoning about mutations in the classic Schorr-Waite graph marking algorithm. Finally, one of the most recent works in this direction is that of Hobor and Villard, who employ not only but also a connective which has variously been called overlapping conjunction or sepish, and which can be used to describe overlapping data structures: holds of a heap when and hold for subheaps and whose union is , but which possibly have a nonempty portion in common. Abstractly, can be seen to be a version of the fusion connective of relevance logic. Concurrent separation logic A Concurrent Separation Logic (CSL), a version of separation logic for concurrent programs, was originally proposed by Peter O'Hearn, using a proof rule which allows independent reasoning about threads that access separate storage. O'Hearn's proof rules adapted an early approach of Tony Hoare to reasoning about concurrency, replacing the use of scoping constraints to ensure separation by reasoning in separation logic. In addition to extending Hoare's approach to apply in the presence of heap-allocated pointers, O'Hearn showed how reasoning in concurrent separation logic could track dynamic ownership transfer of heap portions between processes; examples in the paper include a pointer-transferring buffer, and a memory manager. Commenting on the early classical work on interference freedom by Susan Owicki and David Gries, O'Hearn says that explicit checking for non-interference isn't necessary because his system rules out interference in an implicit way, by the nature of the way proofs are constructed. A model for concurrent separation logic was first provided by Stephen Brookes in a companion paper to O'Hearn's. The soundness of the logic had been a difficult problem, and in fact a counterexample of John Reynolds had shown the unsoundness of an earlier, unpublished version of the logic; the issue raised by Reynolds's example is described briefly in O'Hearn's paper, and more thoroughly in Brookes's. At first it appeared that CSL was well suited to what Dijkstra had called loosely connected processes, but perhaps not to fine-grained concurrent algorithms with significant interference. However, gradually it was realized that the basic approach of CSL was considerably more powerful than first envisaged, if one employed non-standard models of the logical connectives and even the Hoare triples. An abstract version of separation logic was proposed that works