Berend van Starkenburg: Sheafeology – Deriving Separation Logic Inside a Sheaf Topos

Speaker: Berend van Starkenburg (Leiden University)

Abstract: Separation logic is a logic for local reasoning and gluing of compatible resources. From heap cells to probabilistic information. I will present “sheafeology”: an internal, sheaf-theoretic account that derives the separating connective from covers and gluing, rather than postulating it. The benefit is modularity: different flavours of separation logic can coexist in one framework, because they arise from the same local-to-global principle while varying only in what counts as a “resource”.

Technically, we internalise a fibrational account of first-order logic in a sheaf topos. Predicates are subsheaves over resource sheaves; $P * Q$ holds when a cover splits a resource into compatible local views where $P$ and $Q$ hold, and the sheaf gluing axiom amalgamates these views to a global one. When a suitable monoidal structure is present, this coincides with the Day-convolution presentation, but a resource monoid is not required.

I will instantiate the construction to heaps (recovering strong and weak separation) and to a probabilistic setting over countable sets and surjections where $P * Q$ captures probabilistic independence up to surjective refinement.