Skip to Main content Skip to Navigation
Conference papers

Temporary Read-Only Permissions for Separation Logic

Arthur Charguéraud 1, 2 François Pottier 3
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
2 CAMUS - Compilation pour les Architectures MUlti-coeurS
Inria Nancy - Grand Est, ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
3 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
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.
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/hal-01408657
Contributor : Arthur Charguéraud Connect in order to contact the contributor
Submitted on : Monday, January 30, 2017 - 4:46:20 PM
Last modification on : Friday, January 21, 2022 - 3:15:25 AM

File

Vignette du document
readonlysep.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01408657, version 2

Collections

INRIA | INRIA2 | CNRS | UMR8623 | LRI-VALS | ENGEES | UNIV-PARIS-SACLAY | INC-CNRS | SITE-ALSACE | INSA-STRASBOURG | INSA-GROUPE | ANR | GS-COMPUTER-SCIENCE | LRN

Citation

Arthur Charguéraud, François Pottier. Temporary Read-Only Permissions for Separation Logic. Proceedings of the 26th European Symposium on Programming (ESOP 2017), Apr 2017, Uppsala, Sweden. ⟨hal-01408657v2⟩

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

355

Files downloads

263

 

Contact                    Legal Notice                    Personal Data