On the relation between concurrent separation logic and concurrent Kleene algebra
From MaRDI portal
Publication:2347904
DOI10.1016/j.jlamp.2014.08.002zbMath1330.03072OpenAlexW2010194199WikidataQ114851606 ScholiaQ114851606MaRDI QIDQ2347904
Akbar Hussain, Jules Villard, Rasmus L. Petersen, Peter W. O'Hearn
Publication date: 10 June 2015
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlamp.2014.08.002
Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Other algebras related to logic (03G25)
Related Items
An algebraic glimpse at bunched implications and separation logic, A Discrete Geometric Model of Concurrent Program Execution, Unnamed Item, Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Algebraic separation logic
- Concurrent Kleene algebra and its foundations
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
- Algebraic and coalgebraic methods in the mathematics of program construction. International summer school and workshop, Oxford, GB, April 10--14, 2000. Revised lectures
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- In praise of algebra
- An Event Structure Model for Probabilistic Concurrent Kleene Algebra
- Fictional Separation Logic
- The Laws of Programming Unify Process Calculi
- Views
- Subjective auxiliary state for coarse-grained concurrency
- On Locality and the Exchange Law for Concurrent Processes
- Independence and concurrent separation logic
- A Marriage of Rely/Guarantee and Separation Logic
- Reasoning about Optimistic Concurrency Using a Program Logic for History
- Modular Safety Checking for Fine-Grained Concurrency
- Deny-Guarantee Reasoning
- A Basis for Verifying Multi-threaded Programs
- Laws of programming
- The Logic of Bunched Implications
- Refinement Calculus
- Verifying linearizability with hindsight
- BI as an assertion language for mutable data structures
- Permission accounting in separation logic
- Modular Reasoning about Separation of Concurrent Data Structures
- Verifying Concurrent Memory Reclamation Algorithms with Grace
- On closed categories of functors
- Precision and the Conjunction Rule in Concurrent Separation Logic
- Concurrent Separation Logic and Operational Semantics
- On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
