Events

Date: 10 July 2026   Time: 15:00 - 16:00

Location: Room 4.24. Peter Landin Building, Mile End. E1 4NS Map 

This Friday we will have two speakers. The first is by Vorashil Farzaliyev:

Title:
The Frame Rule for Free: Traced Monoidal Semantics of Separation Logic
Vorashil Farzaliyev

Abstract:
Separation logic owes its power to the Frame Rule, which enables local reasoning
about heap-manipulating programs. Calcagno, O'Hearn, and Yang proved that the
syntactic Frame Rule is sound for a command if and only if that command satisfies
the semantic Locality Condition. We exploit this equivalence to construct a separation logic in
which the Frame Rule is not a primitive rule but an admissible consequence of the
underlying categorical structure.

Concretely, we build a traced symmetric monoidal category $\mathcal{S}_\PP^L$
whose morphisms are strict relations over pointer-program states. We generalise
Calcagno et al.'s locality condition from single-state transformers to multi-wire
morphisms - General Local Actions - and prove that locality is
preserved by composition, tensor product, and trace. The trace operator is
realised as the Kleene star of the feedback block, and the five
Joyal--Street--Verity trace axioms are verified algebraically using Conway
semiring identities.

A verification functor into a Hoare category yields a sound and relatively
complete separation logic whose proof system comprises only four structural
inference rules and one generic axiom. The Frame Rule is not among them: because
every morphism of the category satisfies the locality condition, the Frame Rule
is admissible - any triple it could produce is already derivable from the
structural rules alone.