Separation Logic with Monadic Inductive Definitions and Implicit Existentials
Abstract elided by the publisher.
Related papers
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic APLAS 2016
- Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS 2019
- Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL 2026
- Implicit dynamic frames TOPLAS 2012
- Inductive reasoning about effectful data types ICFP 2007
- Fulminate: Testing CN Separation-Logic Specifications in C POPL 2025
- Transfinite Iris: resolving an existential dilemma of step-indexed separation logic PLDI 2021
- Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic ECOOP 2009