Email Gateway (May 30 2022 at 11:43): Email Gateway (May 30 2022 at 11:43):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce the second instalment of a major work on separation logics, by Thibault Dardinier:
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand
Many separation logics support fractional permissions to distinguish between read and write access to a heap location… . In this entry, we formalize a novel, restricted definition of the magic wand, described in a paper at CAV 22, which we call the combinable wand. We prove some key properties of the combinable wand; in particular, a combinable wand is combinable if its right-hand side is combinable.
You will find it online at https://www.isa-afp.org/entries/Combinable_Wands.html
Larry Paulson
Last updated: Jul 15 2022 at 23:21 UTC