I just learned that our (with Nick Benton and Jan Hoffmann) paper, Higher-Order Functional Reactive Programming in Bounded Space, was accepted for publication at POPL 2012!
I am very happy with this work, since it resolves some of the thorniest problems in FRP (memory usage and space leaks) without giving up the highly expressive higher-order abstractions that makes FRP attractive in the first place.
A technical surprise in this work is that this stuff is the first place I've seen where the magic wand of separation logic is actually essential. The denotational model in this paper is a variation on Martin Hofmann's length space model, which forms a doubly-closed category modelling bunched implications. In this paper, we needed both function spaces: we needed the linear function space to control allocation, and we needed the ordinary function space to make use of sharing.
It would be interesting to see if there are ways to transport some of these ideas back to Hoare-style separation logic to find some interesting new invariants.
I am very happy with this work, since it resolves some of the thorniest problems in FRP (memory usage and space leaks) without giving up the highly expressive higher-order abstractions that makes FRP attractive in the first place.
A technical surprise in this work is that this stuff is the first place I've seen where the magic wand of separation logic is actually essential. The denotational model in this paper is a variation on Martin Hofmann's length space model, which forms a doubly-closed category modelling bunched implications. In this paper, we needed both function spaces: we needed the linear function space to control allocation, and we needed the ordinary function space to make use of sharing.
It would be interesting to see if there are ways to transport some of these ideas back to Hoare-style separation logic to find some interesting new invariants.
No comments:
Post a Comment