Local reasoning about data update

DOI10.1016/J.ENTCS.2007.02.006MaRDI QIDQ2864149zbMATH OpenOpenAlexFDO

Authors Cristiano Calcagno, Philippa Gardner, Uri Zarfaty

Publication date 6 December 2013

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.2007.02.006

zbMATH Keywords

context logicheap updatelocal Hoare reasoningtree update

Mathematics Subject Classification ID

Data structures (68P05) Grammars and rewriting systems (68Q42) Logic in computer science (03B70)

Recommendations

• Local reasoning about tree update
• Reasoning about update logic
• Data Structures with Local Update Operations
• List Update with Locality of Reference
• On list update with locality of reference
• On List Update with Locality of Reference
• scientific article; zbMATH DE number 2087445
• List update with probabilistic locality of reference

Cites work

• scientific article; zbMATH DE number 1722648 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• An axiomatic basis for computer programming
• Anytime, anywhere: modal logics for mobile ambients
• Automata, Languages and Programming
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• BI as an assertion language for mutable data structures
• Context logic and tree update
• Context logic as modal logic, completeness and parametric inexpressivity
• Elimination of spatial connectives in static spatial logics
• Local reasoning about tree update
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• The Logic of Bunched Implications
• The semantics and proof theory of the logic of bunched implications
• Variance analyses from invariance analyses

Cited in

(6)

• List Update with Locality of Reference
• Context logic and tree update
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Footprints in Local Reasoning
• An Introduction to Context Logic
• Local reasoning about tree update

Describes a project that uses

Uses Software

• Smallfoot

This page was built for publication: Local reasoning about data update

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864149)