Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : François Pottier Connect in order to contact the contributor
Submitted on : Friday, November 7, 2014 - 11:42:51 AM
Last modification on : Friday, January 21, 2022 - 3:15:57 AM
Long-term archiving on: : Sunday, February 8, 2015 - 10:25:21 AM


Files produced by the author(s)




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⟩



Les métriques sont temporairement indisponibles