Completeness for a First-Order Abstract Separation Logic

DOI10.1007/978-3-319-47958-3_23zbMath1485.03077arXiv1608.06729OpenAlexW2963723858MaRDI QIDQ3179309

Zhé Hóu, Alwen Tiu

Publication date: 21 December 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1608.06729

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Completeness for a First-Order Abstract Separation Logic ⋮ Proof tactics for assertions in separation logic

Uses Software

• Smallfoot

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the almighty wand
• A semantics for concurrent separation logic
• Fictional Separation Logic
• A theorem prover for Boolean BI
• Nondeterministic Phase Semantics and the Undecidability of Boolean BI
• A Unified Display Proof Theory for Bunched Logic
• Completeness for a First-Order Abstract Separation Logic
• Undecidability of Propositional Separation Logic and Its Neighbours
• Looking at Separation Algebras with Boolean BI-eyes
• The semantics of BI and resource tableaux
• Tableaux and Resource Graphs for Separation Logic
• Automated Theorem Proving for Assertions in Separation Logic with All Connectives
• A Marriage of Rely/Guarantee and Separation Logic
• Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
• The Logic of Bunched Implications
• Separation Logic with One Quantified Variable
• Automated Cyclic Entailment Proofs in Separation Logic
• Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
• Parametric completeness for separation theories
• Proof search for propositional abstract separation logics via labelled sequents
• A proof system for separation logic with magic wand
• Programming Languages and Systems
• The formal strong completeness of partial monoidal Boolean BI

This page was built for publication: Completeness for a First-Order Abstract Separation Logic