Email Gateway (Aug 18 2022 at 19:39): Email Gateway (Aug 18 2022 at 19:39):From: Tobias Nipkow <nipkow@in.tum.de>
Separation Algebra
Gerwin Klein and Rafal Kolanski and Andrew Boyton
We present 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 the ITP 2012 rough diamond
"Mechanised Separation Algebra" by the authors.
The aim of this work is to support and significantly reduce the effort for
future separation logic developments in Isabelle/HOL by factoring out the part
of separation logic that can be treated abstractly once and for all. This
includes developing typical default rule sets for reasoning as well as automated
tactic support for separation logic.
http://afp.sourceforge.net/entries/Separation_Algebra.shtml
Last updated: Apr 25 2024 at 20:15 UTC