IT University of Copenhagen
4pm Tuesday, 8th June, 2010
Room 4.31/33, Informatics Forum
The enriched effect calculus (EEC) is a calculus proposed by Egger, Møgelberg and Simpson as a system for reasoning about linear usage of effects.
In this talk we show how EEC can be used as a language capturing stateful computation. Precisely we show that the linear state monad translation from a call-by-value language with store into EEC is fully complete in the sense that any term in EEC of a translated type corresponds to a unique program via the translation. The result is not specific to store, but can be applied to any computational effect expressible using algebraic operations in the sense of Plotkin and Power, even to effects that are not usually thought of as stateful. We give a semantic proof based on the observation that any model of EEC contains a state object and that algebraic operations in the EEC model correspond to certain operations on the state object, which we call "state access operations".
As a detailed example we treat local store, i.e., store in which fresh cells can be allocated. We axiomatize a notion of state object for local store and show how to model this in Pitts' category of nominal sets with restriction structure.
This is joint work with Sam Staton.