1 This directory contains a generic type class implementation of separation

     2 algebra for Isabelle/HOL as well as lemmas and generic tactics which can be

     3 used directly for any instantiation of the type class.

     4 

     5 The ex directory contains example instantiations that include structures such

     6 as a heap or virtual memory.

     7 

     8 The abstract separation algebra is based upon "Abstract Separation Logic" by

     9 Calcagno et al. These theories are also the basis of "Mechanised Separation

    10 Algebra" by Klein et al.

    11