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.

Research notes

I think I will keep some research notes online. I've tried installing MathJax, so this should not be too unreadable, either. Let me begin with the typing of the simply typed lambda calculus, as is traditional.
\[
\begin{array}{lcl}
A & ::= & 1 \bnfalt A \times B \bnfalt A \to B \\
e & ::= & () \bnfalt (e,e) \bnfalt \fst{e} \bnfalt \snd{e} \\
& | & x \bnfalt e\;e' \bnfalt \fun{x:A}{e}
\end{array}
\]

\[
\begin{array}{ll}
\rule{x:A \in \Gamma}
{\judge{\Gamma}{x}{A}} &
\rule{ }
{\judge{\Gamma}{()}{1}}
\\
& \\
\rule{\judge{\Gamma,x:A}{e}{B}}
{\judge{\Gamma}{\fun{x:A}{e}}{A \to B}} &
\rule{\judge{\Gamma}{e}{A \to B} & \judge{\Gamma}{e'}{A}}
{\judge{\Gamma}{e\;e'}{B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A} & \judge{\Gamma}{e'}{B}}
{\judge{\Gamma}{(e,e')}{A \times B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\fst{e}}{A}} &
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\snd{e}}{B}}
\end{array}
\]