Fractional Resources in Unbounded Separation Logic
summary
Defines a new semantics where assertions may temporarily use unbounded states that allow more-than-one permission during evaluation, then reimpose 0–1 permission bounds at statement boundaries to preserve the frame rule. This reconciles the prior semantic vs syntactic notions of fractional multiplication, proves distributivity, factorisability and combinability for star and magic wand, formalises everything in Isabelle/HOL, and gives a clear path to add fractional magic-wand support to tools like Viper and VeriFast.
AI-written summary · about