LFCS Seminar: 18 February 2020 - Miriam Polzer

Title: Local Local Reasoning: Separation Logic for Full Ground Store

Abstract:

We construct categorical semantics of a higher order separation logic over local store, i.e. a logic meant for programs with dynamic memory allocation and automatic garbage collection. Facilitating methods known from topos theory, the main result is an internally complete BI algebra which, contrary to existing generic approaches, does not arise from a monoid object.