The essence of monotonic state

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [31 references]  Display  Hide  Download

https://hal.inria.fr/hal-01081193
Contributor : François Pottier <>
Submitted on : Friday, November 7, 2014 - 11:42:51 AM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Sunday, February 8, 2015 - 10:25:21 AM

File

pilkiewicz-pottier-monotonicit...
Files produced by the author(s)

Identifiers

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. ⟨10.1145/1929553.1929565⟩. ⟨hal-01081193⟩

Share

Metrics

Record views

130

Files downloads

133