Adding Equations to System F

Nick and I have a new draft out, on adding types for term-level equations to System F. Contrary to the experience of dependent types, this is not a very hairy extension -- in fact, I would not even hesitate to call it simple.

However, it does open the door to all sorts of exciting things, such as many peoples' long-standing goal of putting semantic properties of modules into the module interfaces. This is good for documentation, and also (I would hope) good for compilers --- imagine Haskell, if the Monad typeclass definition also told you (and ghc!)  all the equational rewriting that it was supposed to do.

Higher-Order Functional Reactive Programming in Bounded Space

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.