Higher-order representation predicates in separation logic

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. Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Formal methods Keywords Separation Logic, Representation Predicates.

• Type: Journal
• Year: 2016
• Where: CPP
• Authors: Arthur Charguéraud
• Keywords: Artificial Intelligence, CPP 2016