Prehistory. An important precursor of separation logic is the following early paper in program logic.

•Some techniques for proving programs which alter data structures. R.M. Burstall. Machine Intelligence 7, 1972.

A key moment is when Burstall gives a proof of a list-reversal program, which he considers unacceptably tedious, and he says `instead we will try to do better'. Note that Burstall's system is theoretically adequate, and one could have probably proved a completeness theorem for it, etc, etc... but it wasn't good enough for him (one of my favourite pieces of self-criticism). Burstall then goes on to define "distinct non-repreating list systems" (dnrl's), which are not dissimilar to the specialized abstract domains used in heap analysis tools in the 2000s. He observes that computation steps which alter one component of a dnrl automatically leave the other components unchanged, and this short-circuits nasty aliasing problems that became problematic in subsequent proof techniques for pointers, allowing proofs to become considerably shorter.

A different kind of precursor was the logic of bunched implications (BI), introduced in

•The Logic of Bunched Implications P.W. O'Hearn and D. J. Pym. Bulletin of Symbolic Logic , 5(2), June 1999, pp215-244

BI had a general model theory oriented around ``resource composition''. It did not, though, have Hoare triples or other methods of specifying change, and we did not (at that point) know how to construe heaps as models of BI. BI, though, is a general logic with a proof theory and model theory built up in the way of logicians. Pym has written a comprehensive monograph on BI. See the BI page for that and other papers.

History. The first major step in what we now recognize as separation logic was made by John Reynolds, who picked up from Burstall but replaced the specialized dnrl's by a general logical connective for expressing separation (the separating conjunction), and gave Hoare Logic-style axioms for heap mutation that considerably generalized Burstall's treatment.

•Intuitionistic Reasoning about Shared Mutable Data Structure. John Reynolds. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford--Microsoft Symposium in Honour of Sir Tony Hoare

A remarkable part of Reynolds's paper is the realization of how the separating conjunction fits together naturally with inductive definitions of data structures. He was able to give proofs of imperative programs mutating data structures by unpacking definitions (sometimes using logical inference beyond unrolling), mutating an assertion in place, and then repacking the definition again. This lead to proofs of some imperative programs almost as simple as those usually associated with pure functional programs. (Only "almost" because the base cases are sometimes trickier, both logically and in the programs.)

The next step brought in the other precursor.

•BI as an Assertion Language for Mutable Data Structures. Samin Ishtiaq, Peter O'Hearn. Proceedings of POPL'01. PDF version

Armed with Pym's resource semantics, Ishtiaq and I were able to see how the ideas in Reynolds's paper could be reworked for a model that satisfied all the laws of classical (rather than intuitionistic) logic; this model also allowed for an account of memory disposal, and we were (surprisingly to us) now in the territory of "unsafe" low-level programming. The paper is also the first where the `frame rule' appeared: this allowed the local nature of the reasoning steps employed by Reynolds and Burstall to be extended from primitive program statements (e.g., mutating a single pointer) to any operation, including compound operations and entire procedures. This is the key to modular and scalable reasoning.

I am often asked: how are BI and separation logic related, are they the same thing? There are two parts to the answer. First, separation logic is a formalism of program dynamics, based on Hoare triples, where there are no Hoare triples in BI. So, for this part of the answer separation logic is an extension of BI. Second, separation logic has been based on particular storage models while, as Pym has emphasized, BI can be understood more generally in terms of resource and it's model theory which is inspired by a primitive of resource composition. The heap models of separation logic are specific BI models, and furthermore not all BI models are about separation. So, for this second part to the answer, the relation is like that of First-order logic (which is generic) to Peano Arithmetic (a specific theory); the pre- and postconditions of separation logic form a specialization of BI.

After these first papers came one which concentrated on what I called local reasoning: the principle that reasoning and specs can concentrate on only the cells touched by a program component, avoiding to even mention other cells. See in particular the thought experiment involving the ``small axioms'', and an example showing why one can't avoid the notorious frame problem in program specification. The paper also includes a programming language that permits address arithmetic, taking us further away still from the "safe" programming languages we started with.

•Local Reasoning about Programs that Alter Data Structures Peter O'Hearn, John Reynolds, Hongseok Yang. Invited paper, Proceedings of CSL'01, Paris, 2001. Pages 1-19, LNCS 2142 .   PDF version , Slides from talk

A followup paper investigates the semantic basis of the ``frame rule'', for a concrete operational semantics.

•A Semantic Basis for Local Reasoning . Hongseok Yang, Peter O'Hearn. Proceedings of FOSSACS'02. PDF version

Curiously, a confusion has sometimes arisen as to whether separation logic is in some way necessary for local reasoning (or whether we have claimed so). The answer is no. The main semantic discovery, as explained in the FOSSACS paper, it that a host of invariant assertions are automatically true given a certain interpretation of Hoare triples (the "tight" interpretation), and this is independent of the syntactic language used to describe the assertions: separation logic just gives a convenient way to exploit this fact in an inference system .

When you see the CSL'01 or LICS'02 paper for the first time, it is possible to think: well, that was easy! (In a way, that's of course a good thing.) But, for a deeper understanding it helps a lot to consider what came before. For this, I recommend Proving Pointer Programs in Hoare Logic , by Richard Bornat. It shows various struggles, and points to previous work which is worth going back to check up on. It also has a very nice idea: Bornat reveals the relevant portion of storage in all his predicate definitions, which might be thought of as a precursor to the possible worlds in separation logic, and which could even be the basis of an approach to local reasoning without separation logic (see also remarks in the intro to Semantic Basis above).

Continuing... the basic idea of local reasoning was already touched upon in the POPL'01 paper, and pointed at in the previous work of Bornat; it fully crystallized in discussions with Hongseok Yang leading up to the CSL'01 paper. During these discussions Yang came up with examples of ``within data structure'' locality, which went beyond the ``between data structure'' locality that had been displayed in the POPL'01 paper. This showed that the formalism could be used to concentrate on ``local surgeries'' that worked on small areas of a data structure, to be later glued together using the frame rule. Several examples were produced (using varieties of trees), before Yang settled on using the Schorr-Waite graph marking algorithm to illustrate his points.

1. •An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm          H. Yang, SPACE 2001 workshop, London, January 2001
   

Finally, Reynolds's paper from his LICS'02 invited lecture charts developments in separation logic up to May 2002, which represents a natural end-point to the early days.

•Separation Logic: A Logic for Shared Mutable Data Structures

      John Reynolds. Proceedings of LICS 2002. pp55-74