Generic separation logic
Hoare logic
Separation logic
Soundness of Hoare logic
Mechanized semantic library
Separation algebras
Operators on separation algebras
First-order separation logic
A little case study
Covariant recursive predicates
Share accounting
Higher order separation logic
Separation logic as a logic
From separation algebras to separation logic
Simplification by rewriting
Introduction to step-indexing
Predicate implication and subtyping
General recursive predicates
Case study: separation logic with first-class functions.
OBNB doesn't sell books, but you may be able to find a copy at one of these websites:
Program logics for certified compilers by Andrew W. Appel. ISBN 9781107048010. Published by Cambridge University Press in 2014. Publication and catalogue information, links to buy online and reader comments.
