[isabelle] New AFP entry: Separation Algebra
- To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New AFP entry: Separation Algebra
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Fri, 11 May 2012 13:51:35 +0200
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:12.0) Gecko/20120428 Thunderbird/12.0.1
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and