Formalised Inductive Reasoning in the Logic of Bunched Implications
No abstract available.
Related papers
- Semantic cut elimination for the logic of bunched implications, formalized in Coq CPP 2022
- A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency OOPSLA 2022
- Proof search for propositional abstract separation logics via labelled sequents POPL 2014
- Quantified Underapproximation via Labeled Bunches OOPSLA 2025
- Classical BI: a logic for reasoning about dualising resources POPL 2009
- Bunched Fuzz: Sensitivity for Vector Metrics ESOP 2023
- A probabilistic separation logic POPL 2020
- Structuring the verification of heap-manipulating programs POPL 2010