Separation logic through a new lens
Sarah Rovner-Frydman (Marlboro College)
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.
category theory
Audience: researchers in the topic
Series comments: We will have discussions on the new Category Theory Zulip: categorytheory.zulipchat.com
See more information at this blog post.
| Organizers: | Joe Moeller, Christian Williams, John C. Baez* |
| *contact for this listing |