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.