Email Gateway (Aug 22 2022 at 14:38): Email Gateway (Aug 22 2022 at 14:38):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new entry in the AFP, and what’s particularly nice is that it builds on another entry by different authors. Title and abstract below, and you will find it online here: https://www.isa-afp.org/entries/Separata.shtml
Larry Paulson
Separata: Isabelle tactics for Separation Algebra
We bring the labelled sequent calculus $LS_{PASL}$ for propositional abstract separation logic to Isabelle. The tactics given here are directly applied on an extension of the Separation Algebra in the AFP. In addition to the cancellative separation algebra, we further consider some useful properties in the heap model of separation logic, such as indivisible unit, disjointness, and cross-split. The tactics are essentially a proof search procedure for the calculus $LS_{PASL}$. We wrap the tactics in an Isabelle method called separata, and give a few examples of separation logic formulae which are provable by separata.
Last updated: Apr 20 2024 at 08:16 UTC