Skip to Main content Skip to Navigation
Conference papers

Higher-order representation predicates in separation logic

Abstract : In Separation Logic, representation predicates are used to describe mutable data structures, by establishing a relationship between the entry point of the structure, the piece of heap over which this structure spans, and the logical model associated with the structure. When a data structure is polymorphic, such as in the case of a container, its representation predicate needs to be parameterized not just by the type of the items stored in the structure, but also by the representation predicates associated with these items. Such higher-order representation predicates can be used in particular to control whether containers should own their items. In this paper, we present, through a collection of practical examples, solutions to the challenges associated with reasoning about accesses into data structures that own their elements.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-01408670
Contributor : Arthur Charguéraud <>
Submitted on : Monday, December 5, 2016 - 11:23:12 AM
Last modification on : Thursday, July 8, 2021 - 3:49:23 AM
Long-term archiving on: : Monday, March 20, 2017 - 9:54:23 PM

File

horepr.pdf
Files produced by the author(s)

Identifiers

Citation

Arthur Charguéraud. Higher-order representation predicates in separation logic. Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), Jan 2016, St. Petersburg, FL, United States. pp.3 - 14, ⟨10.1145/2854065.2854068⟩. ⟨hal-01408670⟩

Share

Metrics

Record views

321

Files downloads

303