Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Temporary Read-Only Permissions for Separation Logic

Abstract : We present an extension of Separation Logic with a general mechanism for temporarily converting any assertion (or "permission") to a read-only form. No accounting is required: our read-only permissions can be freely duplicated and discarded. We argue that, in circumstances where mutable data structures are temporarily accessed only for reading, our read-only permissions enable more concise specifications and proofs. The metatheory of our proposal is verified in Coq.
Complete list of metadatas

https://hal.inria.fr/hal-01408657
Contributor : Arthur Charguéraud <>
Submitted on : Monday, December 5, 2016 - 11:16:31 AM
Last modification on : Monday, December 9, 2019 - 5:24:07 PM
Document(s) archivé(s) le : Tuesday, March 21, 2017 - 9:37:02 AM

File

readonlysep.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01408657, version 1

Citation

Arthur Charguéraud, François Pottier. Temporary Read-Only Permissions for Separation Logic. 2016. ⟨hal-01408657v1⟩

Share

Metrics

Record views

64

Files downloads

21