Separation Logic II: recursive predicates

I discuss separation logic basics some more, as presented in the seminal paper by John C. Reynolds.  An important idea is describing data structure using separating conjunction and recursive predicates.