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. Feb 18 2020 16.00 - 17.00 LFCS Seminar: 18 February 2020 - Miriam Polzer Speake: Miriam Polzer Informatic Forum G.03
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. Feb 18 2020 16.00 - 17.00 LFCS Seminar: 18 February 2020 - Miriam Polzer Speake: Miriam Polzer Informatic Forum G.03
