BEGIN:VCALENDAR
VERSION:1.0
PRODID:Faculty of Science and Engineering - Research
BEGIN:VEVENT
SUMMARY:The Frame Rule for Free: Traced Monoidal Semantics of Separation Logic
DESCRIPTION;ENCODING=QUOTED-PRINTABLE: This Friday we will have two speakers. The first is by Vorashil Farzaliyev:=0D=0A=
=0D=0A=
Title: =0D=0A=
The Frame Rule for Free: Traced Monoidal Semantics of Separation Logic=0D=0A=
Vorashil Farzaliyev=0D=0A=
=0D=0A=
Abstract:=0D=0A=
Separation logic owes its power to the Frame Rule, which enables local reasoning=0D=0A=
about heap-manipulating programs. Calcagno, O'Hearn, and Yang proved that the=0D=0A=
syntactic Frame Rule is sound for a command if and only if that command satisfies=0D=0A=
the semantic Locality Condition. We exploit this equivalence to construct a separation logic in=0D=0A=
which the Frame Rule is not a primitive rule but an admissible consequence of the=0D=0A=
underlying categorical structure.=0D=0A=
=0D=0A=
Concretely, we build a traced symmetric monoidal category $\mathcal{S}_\PP^L$=0D=0A=
whose morphisms are strict relations over pointer-program states. We generalise=0D=0A=
Calcagno et al.'s locality condition from single-state transformers to multi-wire=0D=0A=
morphisms - General Local Actions - and prove that locality is=0D=0A=
preserved by composition, tensor product, and trace. The trace operator is=0D=0A=
realised as the Kleene star of the feedback block, and the five=0D=0A=
Joyal--Street--Verity trace axioms are verified algebraically using Conway=0D=0A=
semiring identities.=0D=0A=
=0D=0A=
A verification functor into a Hoare category yields a sound and relatively=0D=0A=
complete separation logic whose proof system comprises only four structural=0D=0A=
inference rules and one generic axiom. The Frame Rule is not among them: because=0D=0A=
every morphism of the category satisfies the locality condition, the Frame Rule=0D=0A=
is admissible - any triple it could produce is already derivable from the=0D=0A=
structural rules alone.
LOCATION: Room 4.24. Peter Landin Building, Mile End. E1 4NS
DTSTART:20260710T150000
DTEND:20260710T160000
END:VEVENT
END:VCALENDAR