[isabelle] New AFP entry: A Separation Logic Framework for Imperative HOL



Peter Lammich and Rene Meis
http://afp.sourceforge.net/entries/Separation_Logic_Imperative_HOL.shtml

We provide a framework for separation-logic based correctness proofs of
Imperative HOL programs. Our framework comes with a set of proof methods to
automate canonical tasks such as verification condition generation and frame
inference. Moreover, we provide a set of examples that show the applicability of
our framework. The examples include algorithms on lists, hash-tables, and
union-find trees. We also provide abstract interfaces for lists, maps, and sets,
that allow to develop generic imperative algorithms and use data-refinement
techniques.

As we target Imperative HOL, our programs can be translated to efficiently
executable code in various target languages, including ML, OCaml, Haskell, and
Scala.

Enjoy!





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.