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.
Unable to display preview. Download preview PDF.
- 1.Gerard Berry and Laurent Cosserat. The Esterel synchronous programming language and its mathematical semantics. In A. W. Roscoe S. D. Brookes and editors G. Winskel, editors, Seminar on Concurrency, volume 197 of Lect. Notes in Computer Science, pages 389–448. Springer Verlag, 1985.Google Scholar
- 2.Gerard Berry and the Esterel Team. The Esterel v5.21 System Manual. Centre de Mathématiques Appliquées, Ecole des Mines de Paris and INRIA, March 1999. Available at http://www.inria.fr/meije/esterel.
- 3.Paul Caspi, Halbwachs Halbwachs, Nicolas Pilaud, and John A. Plaice. Lustre: A declarative language for programming synchronous systems. In the Symposium on Principles of Programming Languages (POPL’ 87), January 1987.Google Scholar
- 4.Paul Caspi and M. Pouzet. Synchronous Kahn networks. In International Conference on Functional Programming. ACM SIGPLAN, May 1996.Google Scholar
- 5.Antony Courtney and Conal Elliott. Genuinely functional user interfaces. In Haskell Workshop, 2001.Google Scholar
- 6.Conal Elliott and Paul Hudak. Functional reactive animation. In International Conference on Functional Programming, pages 163–173, June 1997.Google Scholar
- 7.John Peterson et al. Haskell 1.4: A non-strict, purely functional language. Technical ReportYALEU/DCS/RR-1106, Department of Computer Science, Yale University, Mar 1997. World Wide Web version at http://haskell.cs.yale.edu/haskell-report.
- 8.Thierry Gautier, Paul Le Guernic, and Loic Besnard. Signal: A declarative language for synchronous programming of real-time systems. In Gilles Kahn, editor, Functional Programming Languages and Computer Architecture, volume 274 of Lect Notes in Computer Science, edited by G. Goos and J. Hartmanis, pages 257–277. Springer-Verlag, 1987.Google Scholar
- 9.William L. Harrison and Samuel N. Kamin. Modular compilers based on monad transformers. In Proceedings of the IEEE International Conference on Computer Languages, 1998.Google Scholar
- 10.Constance Heitmeyer. Applying Practical formal methods to the specification and analysis of security properties. In Proc. Information Assurance in Computer Networks, LNCS 2052, St. Petersburg, Russia, May 2001. Springer-Verlag.Google Scholar
- 11.Constance Heitmeyer, James Kirby, Bruce Labaw, and Ramesh Bharadwaj. SCR*: A toolset for specifying and analyzing software requirements. In Proc. Computer-Aided Verification, Vancouver, Canada, 1998.Google Scholar
- 12.Paul Hudak. The Haskell School of Expression-Learning Functional Programming through Multimedia. Cambridge University Press, New York, 2000.Google Scholar
- 13.Microchip Technology Inc. PIC16C66 Datasheet. Available on-line at http://www.microchip.com/.
- 14.John Peterson, Gregory Hager, and Paul Hudak. A language for declarative robotic programming. In International Conference on Robotics and Automation, 1999.Google Scholar
- 15.Alastair Reid, John Peterson, Greg Hager, and Paul Hudak. Prototyping realtime vision systems: An experiment in DSL design. In Proceedings of International Conference on Software Engineering, May 1999.Google Scholar
- 16.Robo Cup official site. http://www.robocup.org/.
- 17.Walid Taha, Paul Hudak, and Zhanyong Wan. Directions in functional programming for real(-time) applications. In Thomas A. Henzinger and Christoph M. Kirsch, editors, Proc. First International Workshop, EMSOFT, LNCS 2211, pages 185–203, Tahoe City, CA, USA, October 2001. Springer-Verlag.Google Scholar
- 18.Walid Taha and Tim Sheard. Multi-stage programming with explicit annotations. In Proceedings of Symposium on Partial Evaluation and Semantics Based Program manipulation, pages 203–217. ACM SIGPLAN, 1997.Google Scholar
- 19.Zhanyong Wan and Paul Hudak. Functional reactive programming from first principles. In Proceedings of Symposium on Programming Language Design and Implementation. ACM, 2000.Google Scholar
- 20.Zhanyong Wan, Walid Taha, and Paul Hudak. Real-time FRP. In Proceedings of Sixth ACM SIGPLAN International Conference on Functional Programming, Florence, Italy, September 2001. ACM.Google Scholar