BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Sarah Rovner-Frydman (Marlboro College) DTSTART:20200506T170000Z DTEND:20200506T180000Z DTSTAMP:20260423T024508Z UID:ACTUCR/4 DESCRIPTION:Title: S eparation logic through a new lens\nby Sarah Rovner-Frydman (Marlboro College) as part of ACT@UCR\n\n\nAbstract\nSeparation logic aims to reason compositionally about the behavior of programs that manipulate shared res ources. When working with separation logic\, it is often necessary to mani pulate information about program state in patterns of deconstruction and r econstruction. 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 t he literature for managing these patterns of manipulation can be derived a s 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 f amiliar\, and it reveals that much of it was already hiding in separation logic in plain sight.\n LOCATION:https://researchseminars.org/talk/ACTUCR/4/ END:VEVENT END:VCALENDAR