LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Communication dans un congrès
Proceedings of the 26th European Symposium on Programming (ESOP 2017), Apr 2017, Uppsala, Sweden
https://hal.inria.fr/hal-01408657
Contributeur : Arthur Charguéraud
<>
Soumis le : lundi 30 janvier 2017 - 16:46:20
Dernière modification le : lundi 26 novembre 2018 - 13:28:02
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〉
