Separation Logic Formalization

Formalization of separation logic using the Isabelle/HOL proof assistant, as well as the proof of formula rewriting results from a paper entitled “The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains”.