Separation Logic Semantics for Communicating Processes

DOI10.1016/j.entcs.2008.04.050zbMath1286.68352MaRDI QIDQ5415605

Peter W. O'Hearn, C. A. R. Hoare

Publication date: 13 May 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.04.050

zbMATH Keywords

concurrency; separation logic; communicating sequential processes; semantics of programming languages

Mathematics Subject Classification ID

68N15: Theory of programming languages

03B70: Logic in computer science

68Q55: Semantics in the theory of computing

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Related Items

Propositional Dynamic Logic with Storing, Recovering and Parallel Composition, A calculus and logic of bunched resources and processes, Event algebra for transition systems composition application to timed automata, Denotational semantics of channel mobility in UTP-CSP, Mechanized semantics for the clight subset of the C language

Uses Software

• occam-pi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A calculus and logic of resources and processes
• A semantics for concurrent separation logic
• Resources, concurrency, and local reasoning
• A calculus of durations
• The semantics and proof theory of the logic of bunched implications
• Context logic as modal logic
• The Logic of Bunched Implications
• Anytime, anywhere
• Permission accounting in separation logic
• Footprints in Local Reasoning
• Communicating Sequential Processes. The First 25 Years
• Structured Communication-Centred Programming for Web Services