This directory contains a generic type class implementation of separation+
−
algebra for Isabelle/HOL as well as lemmas and generic tactics which can be+
−
used directly for any instantiation of the type class.+
−
+
−
The ex directory contains example instantiations that include structures such+
−
as a heap or virtual memory.+
−
+
−
The abstract separation algebra is based upon "Abstract Separation Logic" by+
−
Calcagno et al. These theories are also the basis of "Mechanised Separation+
−
Algebra" by Klein et al.+
−
+
−