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
2 CAMUS - Compilation pour les Architectures MUlti-coeurS
3 GALLIUM - Programming languages, types, compilation and proofs

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.

Domaines: Langage de programmation [cs.PL]

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⟩