Separation Logic Adapted for Proofs by Rewriting

We present a formalisation of separation logic which, by avoiding the use of existential quantifiers, allows proofs that only use standard equational rewriting methods as found in off-the-shelf theorem provers. This proof automation is sufficiently strong to free the user from dealing with low-level details in proofs of functional correctness. The work presented here has been implemented in HOL4 and ACL2. It is illustrated on a standard example (reversal of a linked-list).

• Type: Conference
• Year: 2010
• Where: ITP
• Authors: Magnus O. Myreen
• Keywords: ITP 2010, Mathematics, Off-the-shelf Theorem Provers, Separation Logic, Standard Equational Rewriting