Friday, January 14, 2011

Ultrametric Semantics of Reactive Programs

I've got a new draft paper out with Nick Benton, Ultrametric Semantics of Reactive Programs.

We answer some longstanding open questions in FRP, namely:

1. What are higher-order reactive functions at all? How do you interpret them, and what are their semantics?
2. How can we implement FRP in a reasonable way, without compromising on either the equational theory or the ability to fit into the mutable callback event loop world of MVC?

It's got a little something for everyone -- some very pretty proof theory, some nice denotational semantics, and a hardcore separation logic proof with a step-indexed logical relation.