The essence of monotonic state

Alexandre Pilkiewicz 1 François Pottier 1, *
* Auteur correspondant
Abstract : We extend a static type-and-capability system with new mechanisms for expressing the promise that a certain abstract value evolves monotonically with time; for enforcing this promise; and for taking advantage of this promise to establish non-trivial properties of programs. These mechanisms are independent of the treatment of mutable state, but combine with it to offer a flexible account of "monotonic state". We apply these mechanisms to solve two reasoning challenges that involve mutable state. First, we show how an implementation of thunks in terms of references can be assigned types that reflect time complexity properties, in the style of Danielsson (2008). Second, we show how an implementation of hash-consing can be assigned a specification that conceals the existence of an internal state yet guarantees that two pieces of input data receive the same code if and only if they are equal.
Type de document :
Communication dans un congrès
TLDI 2011: The Sixth ACM SIGPLAN Workshop on Types in Language Design and Implementation, Jan 2011, Austin, United States. 2011, <10.1145/1929553.1929565>
Liste complète des métadonnées


https://hal.inria.fr/hal-01081193
Contributeur : François Pottier <>
Soumis le : vendredi 7 novembre 2014 - 11:42:51
Dernière modification le : lundi 5 octobre 2015 - 17:00:54
Document(s) archivé(s) le : dimanche 8 février 2015 - 10:25:21

Fichier

pilkiewicz-pottier-monotonicit...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Alexandre Pilkiewicz, François Pottier. The essence of monotonic state. TLDI 2011: The Sixth ACM SIGPLAN Workshop on Types in Language Design and Implementation, Jan 2011, Austin, United States. 2011, <10.1145/1929553.1929565>. <hal-01081193>

Partager

Métriques

Consultations de
la notice

83

Téléchargements du document

105