State Passing Style

Speaker(s): Sam Staton (University of Cambridge)
Organiser:
Time: 22/06/2011 13:00-14:00
Location: B53/4025

Abstract

An imperative program of type X -> Y can often be written as a pure functional program in the state passing style, S*X -> S*Y (for a state type S). This makes the changing state explicit.

I will investigate the idea that EVERY computational effect can be treated in the state passing style. I will do this in the context of a metalanguage in which we can enforce the linear use of state: the state cannot be duplicated or discarded. Models of this metalanguage are enriched categories of a certain kind.

This is joint work with Rasmus Møgelberg, building on work by Jeff Egger and Alex Simpson.