Functional Reactive Programming (FRP) is a high-level declarative language for programming reactive systems. Previous work
on FRP has demonstrated its utility in a wide range of application domains, including animation, graphical user interfaces,
and robotics. FRP has an elegant continuous-time denotational semantics. However, it guarantees no bounds on execution time
or space, thus making it unsuitable for many embedded real-time applications. To alleviate this problem, we recently developed
Real-Time FRP (RT-FRP), whose operational semantics permits us to formally guarantee bounds on both execution time and space.
In this paper we present a formally verifiable compilation strategy from a new language based on RT-FRP into imperative code.
The new language, called Event-Driven FRP (E-FRP), is more tuned to the paradigm of having multiple external events. While it is smaller than RT-FRP, it features a
key construct that allows us to compile the language into efficient code. We have used this language and its compiler to generate
code for a small robot controller that runs on a PIC16C66 micro-controller. Because the formal specification of compilation
was crafted more for clarity and for technical convenience, we describe an implementation that produces more efficient code.
Funded by NSF CCR9900957, NSF ITR-0113569, and DARPA F33615-99-C-3013 and DABT63-00-1-0002