Over the past decade, a number of languages for functional reactive
programming (FRP) have been suggested, which use modal types to
ensure properties like causality, productivity and lack of space
leaks. So far, almost all of these languages have included a modal
operator for delay on a global clock. For some applications,
however, a global clock is unnatural and leads to leaky
abstractions as well as inefficient implementations. While modal
languages without a global clock have been proposed, no operational
properties have been proved about them, yet.

This paper proposes Async RaTT, a new modal language for
asynchronous FRP, equipped with an operational semantics mapping
complete programs to machines that take asynchronous input signals
and produce output signals. The main novelty of Async RaTT is a new
modality for asynchronous delay, allowing each output channel to be
associated at runtime with the set of input channels it depends on,
thus causing the machine to only compute new output when
necessary. We prove a series of operational properties including
causality, productivity and lack of space leaks. We also show that,
although the set of input channels associated with an output channel
can change during execution, upper bounds on these can be determined
statically by the type system.