Abstract
Reactive systems respond to concurrent, possibly unsynchronized streams of input events. Programming reactive systems is challenging without language support for event-triggered actions. It is even more challenging to reason about reactive systems. This paper explores a new conceptual basis for applying functional programming techniques to the design and formal verification of reactive systems. The mathematical foundation for this approach is based upon signature coalgebras and derived proof rules for coinduction. The concepts are illustrated with an example that has been used with the language Esterel.
The research reported in this paper was supported by the USAF Materiel Command.
Chapter PDF
Similar content being viewed by others
References
Samson Abramsky. A domain equation for bisumulation. Information and Computation, 92:161–218, 1992.
Edward A. Ashcroft and William W. Wadge. Lucid: A non-procedural language with iteration. Communications of the ACM, 20(7):519–526, 1977.
G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science Of Computer Programming 19(2):87–152 1992.
Richard S. Bird. An introduction to the theory of lists. In M. Broy, editor Logic of Programming and Calculi of Discrete Designvolume 36 of NATO Series F. Springer-Verlag, 1986.
G. Boudol, V. Roy, R. de Simone, and D. Vergamini. Process calculi, from theory to practice: Verification tools. In Automatic Verification Methods for Finite State Systems LNCS 407pages 1–10. Springer-Verlag 1990.
R. E. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. ACM Computing Surveys, 24(3):293–318,September 1992.
R M. Burstall and P. J. Landin. Programs and their proofs: an algebraic approach. In Machine Intelligence 4pages 17–44. Edinburgh University Press 1969.
Rod Burstall. Inductively defined functions in functional programming languages. Journal of Computer and System Sciences, 34(2/3):409–421, 1987.
P. Caspi and M. Pouzet. Synchronous Kahn networks. In Proceedings of ACM SIGPLAN Internat. Conf. on Functional Programmingpages 226238. ACM Press, May 1996.
E. M. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In A Decade of Concurrency: Reflections and Perspectivesvolume 803 of Lecture Notes in Computer Sciencepages 124–175. Springer Verlag 1992.
E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronizations skeletons. Science of Computer Programming 2:241–266 1982.
Marcelo P. Fiore. A coinduction principle for recursive data types based on bisimulation. Information and Computation, 127(2):186–198, 1996.
Peter Freyd. Recursive types reduced to inductive types. In Fifth IEEE Symposium on Logic in Computer Sciencepages 498–507. IEEE Computer Society Press 1990.
Andrew Gordon. Bilimilarity as a theory of functional programming In Proceedings of 11th Conference on Mathematical Foundations of Programming Semanticsvolume 1 of Electronic Notes in Theoretical Computer Science. Elsevier URL: www.pigeon.elsevier.nl/mcs/tcs/pc/volumel.htm, 1995.
N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE 79(9):1305–1320 1991.
N. Halbwachs, J.-C. Fernandez, and A. Bouajjanni. An executable temporal logic to express safety properties and its connection with the language Lustre. In Sixth International Symp. on Lucid and Intensional Programming, ISLIP’93,Quebec City, Canada, April 1993. Université Laval.
N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real-time systems by means of the synchronous data-flow programming language lustre. IEEE Transactions on Software Engineering, 18 (9), 1992.
Bart Jacobs. Mongruences and cofree coalgebras. In Algebraic Methodology and Software Technology - AMAST’95, volume 936 of Lecture Notes in Computer Science, pages 245–260. Springer Verlag, 1995.
Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. EACTS Bulletin, 62: 222–259, 1997.
Gilles Kahn The semantics of a simple language for parallel programming. In IFIP’74 Congress. North Holland, 1974.
Richard B. Kieburtz and Jeffrey Lewis. Algebraic Design Language—Preliminary definition. Technical report, Pacific Software Research Center, Oregon Graduate Institute of Science and Technology, January 1994.
Richard B. Kieburtz and Jeffrey Lewis. Programming with algebras. In Advanced Functional Programming, volume 925 of Lecture Notes in Computer Science, pages 267–307. Springer Verlag, 1995.
Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Proc. of 5th ACM Conf. on Functional Programming Languages and Computer Architecture, volume 523 of Lecture Notes in Computer Science, pages 124–144. Springer-Verlag, August 1991.
Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87: 209–220, 1992.
Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation, 7 (2): 175–204, 1997.
Andrew Pitts. A coinduction principle for recursively defined domains. Theoretical Computer Science, 124 (2): 195–219, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Kieburtz, R.B. (1998). Reactive Functional Programming. In: Gries, D., de Roever, WP. (eds) Programming Concepts and Methods PROCOMET ’98. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35358-6_19
Download citation
DOI: https://doi.org/10.1007/978-0-387-35358-6_19
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6299-0
Online ISBN: 978-0-387-35358-6
eBook Packages: Springer Book Archive