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:
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.
Azimuth 
Not listed on mathseminars.org
Or did I skim too quickly?
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
It would seem that the invitation link has expired, and you need an invitation to join.
If you click on “Category Theory Community Server” above you’ll find a working link to become a member. It will expire eventually, but it hasn’t now.
Once you’re a member you can discuss Sarah’s talk here:
https://categorytheory.zulipchat.com/#narrow/stream/229966-ACT.40UCR-seminar/topic/May.204th.3A.20Sarah.20Rovner-Frydman/near/196269053
The link is indeed working, but when I try to sign up, it says “You need an invitation to join this organization.”
I don’t experience what you’re experiencing. Are you going to the URL I recommended:
https://categorytheory.zulipchat.com/join/u4h1nwjtpcr0blvjpg4kzanm/ ?
Yes, that’s the link. Assuming you’re already a member, that’s why it works for you. For me, I am allowed to log in if I am already a member, but “Sign Up” (in the upper-right hand corner) brings me to a page that says “You need an invitation to join this organization.” and has no other login links. (The “Sign in with Google” etc link has the same result.)
I took the first few steps on a browser that didn’t know who I was. The first step was to enter my email and click Sign up in the big dark blue box right underneath where it asks you to enter your email. That will make it send you an email; read that and proceed from there.
Ignore the other thing saying “Sign up” in the upper-right corner — apparently that’s just a trick to weed out people who don’t do the right thing.
Thank you so much — yeah, that was it, I somehow missing the giant “Sign up” in the middle of the page.
Was this recorded?
Yeah, they’re all recorded. Please wait for me to edit the video.