Higher-order representation predicates in separation logic

Arthur Charguéraud 1, 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
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 : 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.
Type de document :
Communication dans un congrès
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), Jan 2016, St. Petersburg, FL, United States. ACM, pp.3 - 14, 2016, 〈10.1145/2854065.2854068〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01408670
Contributeur : Arthur Charguéraud <>
Soumis le : lundi 5 décembre 2016 - 11:23:12
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : lundi 20 mars 2017 - 21:54:23

Fichier

horepr.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. ACM, pp.3 - 14, 2016, 〈10.1145/2854065.2854068〉. 〈hal-01408670〉

Partager

Métriques

Consultations de la notice

177

Téléchargements de fichiers

41