Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: A Separation Logic Framework fo...


view this post on Zulip Email Gateway (Aug 19 2022 at 09:21):

From: Tobias Nipkow <nipkow@in.tum.de>
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!


Last updated: Mar 29 2024 at 01:04 UTC