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

Peter Lammich and Rene Meis

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

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


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