|
25
|
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 |
|