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
Contributor : Arthur Charguéraud Connect in order to contact the contributor
Submitted on : Monday, December 5, 2016 - 11:23:12 AM
Last modification on : Saturday, June 25, 2022 - 10:22:40 PM
Long-term archiving on: : Monday, March 20, 2017 - 9:54:23 PM


Files produced by the author(s)



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⟩



Record views


Files downloads