Abstract

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.

@InProceedings{Wan2002,
  author = 	 "Zhanyong Wan and Walid Taha and Paul Hudak",
  title = 	 "Event-Driven {FRP}",
  booktitle = 	 "Practical Aspects of Declarative Languages ({PADL'02})",
  year = 	 2002,
  month = 	 jan
}

   Download

• efrp.dvi (28k)
• efrp.ps.gz (89k)