LFCS Seminar: Rasmus Møgelberg
Full Abstraction in a Metalanguage for State
What 


When 
Jun 08, 2010 from 04:00 PM to 05:00 PM 
Where  4.31/4.33 
Add event to calendar 
vCal iCal 
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 callbyvalue 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.