Ultrametric Semantics of Reactive Programs: or, How to Prove a GUI Correct

In this talk, I describe a denotational model of higher-order
functional reactive programming using ultrametric spaces and
nonexpansive maps, which provides a natural Cartesian closed
generalization of causal stream functions and uarded recursive
defnitions. To write programs, I also show how to define a normalizing
type theory corresponding to this semantics.

I show how reactive programs written in this language can be
implemented efficiently using an imperatively updated dataflow graph
(with correctness proof, but not in this talk!), and demonstrate how
GUI (graphical user interface) programs look when written in this style.