Separation Logic Through a New Lens

In the sixth talk of the ACT@UCR seminar, Sarah Rovner-Frydman told us about a new approach to separation logic, a way to reason about programs.

She gave her talk on May 6th, 2020. Afterwards we discussed it on the Category Theory Community Server, here:

https://categorytheory.zulipchat.com/#narrow/stream/229966-ACT.40UCR-seminar/topic/May.204th.3A.20Sarah.20Rovner-Frydman/near/196269053

You can view or join the conversation there if you sign in.

You can see her slides here, or download a video of her talk here, or watch the video here:

• Sarah Rovner-Frydman: Separation logic through a new lens.

Abstract. Separation logic aims to reason compositionally about the behavior of programs that manipulate shared resources. When working with separation logic, it is often necessary to manipulate information about program state in patterns of deconstruction and reconstruction. This achieves a kind of “focusing” effect which is somewhat reminiscent of using optics in a functional programming language. We make this analogy precise by showing that several interrelated techniques in the literature for managing these patterns of manipulation can be derived as instances of the general definition of profunctor optics. In doing so, we specialize the machinery of profunctor optics from categories to posets and to sets. This simplification makes most of this machinery look more familiar, and it reveals that much of it was already hiding in separation logic in plain sight.

Rovner_Frydman_diagram

11 Responses to Separation Logic Through a New Lens

  1. Stasheff, James says:

    Not listed on mathseminars.org
    Or did I skim too quickly?

    • John Baez says:

      This talk is actually listed there already! But thanks, I need to put up the titles of the next batch of talks at the ACT@UCR seminar:

      • 13 May: Tai-Danae Bradley – Formal concepts vs. eigenvectors of density operators

      • 20 May: Gordon Plotkin – A complete axiomatisation of partial differentiation

      • 27 May: Simon Willerton – The Legendre–Fenchel transform from a category theoretic perspective

  2. Gregory Travis says:

    It would seem that the invitation link has expired, and you need an invitation to join.

  3. Gregory M Travis says:

    Was this recorded?

You can use Markdown or HTML in your comments. You can also use LaTeX, like this: $latex E = m c^2 $. The word 'latex' comes right after the first dollar sign, with a space after it.

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.