Separation Logic Through a New Lens
Azimuth 2020-05-05
In the sixth talk of the ACT@UCR seminar, Sarah Rovner-Frydman will tell us about a new approach to separation logic, a way to reason about programs.
She’ll give her talk on Wednesday May 5th at 5 pm UTC, which is 10 am in California, or 1 pm on the east coast of the United States, or 6 pm in England. It will be held online via Zoom, here:
https://ucr.zoom.us/j/607160601
Afterwards we’ll discuss her talk at the Category Theory Community Server. You can see those discussions here if you become a member:
• May 6, 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.