Abstract
We review the basics of functional programming, and give a brief introduction to emerging techniques and approaches relevant to buildingreal-time software. In doingso we attempt to explain the relevance of functional programming concepts to the real-time applications domain. In particular, we address the use of types to classify properties of real-time computations.
Funded by DARPA F33615-99-C-3013 and NSF CCR-9900957.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Klaus Aehligand Helmut Schwichtenberg. A syntactical analysis of non-sizeincreasingp olynomial time computation. In the Symposium on Logic in Computer Science (LICS’ 00), pages 84–94. IEEE, June 2000.
Stuart Allen, Robert Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo. The nuprl open logical environment. In D. McAllester, editor, the International Conference on Automated Deduction, volume 1831 of Lecture Notes in Artificial Intelligence, pages 170–176. Springer-Verlag, 2000.
John Backus. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. Communications of the ACM, 21(8):613–641, 1978.
Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, revised edition, 1984.
Henk P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science. Oxford University Press, Oxford, 1991.
Nick Benton and Philip Wadler. Linear logic, monads and the lambda calculus. In the Symposium on Logic in Computer Science (LICS’ 96), New Brunswick, 1996. IEEE Computer Society Press.
Gerard Berry. Real time programming: Special purpose or general purpose languages. In IFIP World Computer Congress, San Francisco, 1989.
Gerard Berry. The constructive semantics of pure Esterel (draft version 3). Draft Version 3, Ecole des Mines de Paris and INRIA, July 1999.
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.
Manfred Broy. A fixed point approach to applicative multi-programming. In Lecture Notes. International Summer School on Theoretical Foundations of Programming Methodology, 1981.
Cristiano Calcagno. Stratified operational semantics for safety and correctness of the region calculus. In the Symposium on Principles of Programming Languages (POPL’01), 2001.
Cristiano Calcagno, Eugenio Moggi, and Walid Taha. Closed types as a simple approach to safe imperative multi-stage programming. In the International Colloquium on Automata, Languages, and Programming (ICALP’ 00), volume 1853 of Lecture Notes in Computer Science, pages 25–36, Geneva, 2000. Springer-Verlag.
Luca Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Reports, pages 431–507. Springer-Verlag, New York, 1991.
Luca Cardelli. Type systems. In Allen B. Jr Tucker, editor, The Computer Science and Engineering Handbook. CRC Press, 1997.
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.
Paul Caspi and Marc Pouzet. Synchronous Kahn networks. In the International Conference on Functional Programming (ICFP’96), pages 226–238, Philadelphia, Pennsylvania,24-26 May 1996.
Alonzo Church. The Calculi of Lambda Conversion. Princeton University Press, Princeton, 1941.
Koen Claessen. Embedded Languages for Describing and Verifying Hardware. PhD thesis, Chalmers, 2001.
J. Robin B. Cockett and Dwight Spencer. Strong categorical datatypes I. In R. A. G. Seely, editor, Proceedings International Summer Category Theory Meeting, Montréal, Québec, 23-30 June 1991, volume 13 of Canadian Mathematical Society Conf. Proceedings, pages 141–169. American Mathematical Society, Providence, RI, 1992.
J. Robin B. Cockett and Dwight Spencer. Strong categorical datatypes II: A term logic for categorical programming. Theoretical Computer Science, 139(1-2):69–113, 1995.
Thierry Coquand and Gérard Huet. A theory of constructions. Presented at the International Symposium on Semantics of Data Types, Sophia-Antipolis, 1984.
Antony Courtney and Conal Elliott. Genuinely functional user interfaces. In Proceedings of the Haskell Workshop, September 2001.
Patrik Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. In Mathematical Foundations of Programming Semantics, 1997.
Karl Crary and Stephanie Weirich. Resource bound certification. In the Symposium on Principles of Programming Languages (POPL’ 00), pages 184–198, N.Y., January 19-21 2000. ACM Press.
Rowan Davies. A temporal-logic approach to binding-time analysis. In the Symposium on Logic in Computer Science (LICS’ 96), pages 184–195, New Brunswick, 1996. IEEE Computer Society Press.
Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In the Symposium on Principles of Programming Languages (POPL’ 96), pages 258–270, St. PetersburgBeac h, 1996.
Roberto Di Cosmo. Isomorphisms of Types: from λ-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhäuser, 1995.
Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Chet Murthy, Catherine Parent, Christine Paulin-Mohring, and Benjamin Werner. The Coq proof assistant user’s guide. Rapport Techniques 154, INRIA, Rocquencourt, France, 1993. Version 5.8.
Abbas Edalat and Peter John Potts. A new representation for exact real numbers. Electronical Notes in Theoretical Computer Science, 6:14 pp., 1997.
Conal Elliott and Paul Hudak. Functional reactive animation. In International Conference on Functional Programming, pages 163–173, June 1997.
John Peterson et. al. Haskell 1.4: A non-strict, purely functional language. Technical Report YALEU/DCS/RR-1106, Department of Computer Science, Yale University, Mar 1997. World Wide Web version at http://haskell.cs.yale.edu/haskell-report.
Cormac Flanagan and Martín Abadi. Types for safe locking. In European Symposium on Programming (ESOP), volume 1576 of Lecture Notes in Computer Science, pages 91–108. Springer-Verlag, 1999.
Robert Glück and Jesper Jorgensen. Fast binding-time analysis for multi-level specialization. In Dines Bjorner, Manfred Broy, and Igor V. Pottosin, editors, Perspectives of System Informatics, volume 1181 of Lecture Notes in Computer Science, pages 261–272. Springer-Verlag, 1996.
Healfdene Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994.
Andrew D. Gordon. Functional Programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press, September 1994.
Carl A. Gunter. Semantics of Programming Languages. MIT Press, 1992.
David Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, June 1987.
Peter Henderson. Functional programming, formal specification and rapid prototyping. IEEE Transactions on Software Engineering, 12(2):241–250, 1986.
J. Roger Hindley. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1997.
C. A. R. Hoare. Communicatingsequen tial processes. Comm. ACM, 21(8):666–677, 1978.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
Wilfred Hodges. A Shorter Model Theory. Cambridge University Press, 1997.
Martin Hofmann. Linear types and non-size-increasingp olynomial time computation. In the Symposium on Logic in Computer Science (LICS’ 99), pages 464–473. IEEE, July 1999.
Martin Hofmann. Programming languages capturing complexity classes. SIGACTN: SIGACT News (ACM Special Interest Group on Automata and Computability Theory), 31, 2000.
Martin Hofmann. A type system for bounded space and functional in-place update. Nordic Journal of Computing, 7(4), Winter 2000.
Paul Hudak. The Haskell School of Expression-Learning Functional Programming through Multimedia. Cambridge University Press, New York, 2000.
Paul Hudak and Joe Fasel. A gentle introduction to Haskell. ACM SIGPLAN Notices, 27(5), May 1992.
R. J. M. Hughes. Why functional programming matters. Technical Report 16, Programming Methodology Group, Chalmers University of Technology, November 1984.
R. J. M. Hughes and Lars Pareto. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming (ICFP-99), volume 34.9 of ACM Sigplan Notices, pages 70–81, N.Y., September 27-29 1999. ACM Press.
R. J. M. Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems usingsized types. In Guy L. Steele Jr, editor, In proceedings of the ACM Symposium on Principles of Programming Languages (POPL), volume 23, St Petersburg, Florida, 1996. ACM Press.
Neil D. Jones. Computability and Complexity From a Programming Perspective. Foundations of Computing. The MIT Press, Cambridge, MA, USA, 1997.
Neil D Jones and C. K. Gomard. A partial evaluator for the untyped lambda calculus. DIKU report, University of Copenhagen, Copenhagen, Denmark, 1990. Extended version of [53].
Neil D. Jones, C. K. Gomard, A. Bondorf, O. Danvy, and T. Mogensen. A selfapplicable partial evaluator for the lambda calculus. In IEEE International Conference on Computer Languages, pages 49–58, 1990.
Richard Kieburtz. Tamingeffects with monadic typing. In the International Conference on Functional Programming (ICFP’ 98), volume 34(1) of ACM SIGPLAN Notices, pages 51–62. ACM, June 1999.
Richard Kieburtz. Real-time reactive programming for embedded controllers. Available from author’s home page, March 2001.
Richard B. Kieburtz. Implementing closed domain-specific languages. In [91], pages 1–2, 2000.
Leslie Lamport. Time, clocks and the orderingof events in a distributed system. Communications of the ACM, 21(7), 1978.
Edward A. Lee. What’s ahead for embedded software? In IEEE Computer, September 2000.
Edward A. Lee. Computingfor embedded systems. In IEEE Instrumentation and Measurement Technology Conference, Budapest, Hungary, 2001.
Xavier Leroy. Objective Caml, 2000. Available from http://caml.inria.fr/ocaml/.
Zhaohui Luo and Robert Pollack. The LEGO proof development system: A user’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, May 1992.
John Matthews, Byron Cook, and John Launchbury. Microprocessor specification in Hawk. In Proceedings of the 1998 International Conference on Computer Languages, pages 90–101. IEEE Computer Society Press, 1998.
Nicholas McKay and Satnam Singh. Dynamic specialization of XC6200 FPGAs by partial evaluation. In Reiner W. Hartenstein and Andres Keevallik, editors, International Workshop on Field-Programmable Logic and Applications, volume 1482 of Lecture Notes in Computer Science, pages 298–307. Springer-Verlag, 1998.
Robin Milner. A Calculus of Communicating Systems, volume 81 of Lecture Notes in Computer Science. Springer-Verlag, 1981.
Robin Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
John C. Mitchell. Foundations for Programming Languages. MIT Press, Cambridge, 1996.
Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991. 202 W. Taha, P. Hudak, and Z. Wan
Andrew Moran and David Sands. Improvement in a lazy context: An operational theory for call-by-need. In the Symposium on Principles of Programming Languages (POPL’ 99), pages 43–56, San Antonio, Texas, January 1999. ACM.
Alan Mycroft and Richard Sharp. A statically allocated parallel functional language. In Automata, Languages and Programming, pages 37–48, 2000.
Flemming Nielson and Hanne Riis Nielson. Two-level semantics and code generation. Theoretical Computer Science, 56(1):59–133, 1988.
Hanne Rijs Nielson and Flenning Nielson. Semantics with Applications: A Formal Introduction. John Wiley & Sons, Chichester, 1992. Available online from http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html.
Bengt Nordström. The ALF proof editor. In Proceedings of the Workshop on Types for Proofs and Programs, pages 253–266, Nijmegen, 1993.
Bengt Nordström, Kent Peterson, and Jan M. Smith. Programming in Martin-Löf’ s Type Theory: An Introduction, volume 7. Oxford University Press, New York, NY, 1990.
Chris Okasaki. Even higher-order functions for parsing or why would anyone ever want to use a sixth-order function? Journal of Functional Programming, 8(2):195–199, March 1998.
Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, Cambridge, UK, 1998.
Oregon Graduate Institute Technical Reports. P.O. Box 91000, Portland, OR 97291-1000,USA. Available online from ftp://cse.ogi.edu/pub/tech-reports/README.html. Last viewed August 1999.
Paul Hudak Simon Peyton Jones, Philip Wadler, Brian Boutel, John Fairbairn, Joseph Fasel, Maria M. Guzman, Kevin Hammond, John Hughes, Thomas Johnsson, Dick Kieburtz, Rishiyur Nikhil, Will Partain, and John Peterson. Report on the programming language Haskell. SIGPLAN Notices, 27(5):Section R, 1992.
Simon Peyton Jones and Philip Wadler. Imperative functional programming. In the Symposium on Principles of Programming Languages (POPL’ 93). January 1993. 71–84.
Frank Pfenningand Carsten Schürmann. System description: Twelf — A metalogical framework for deductive systems. In H. Ganzinger, editor, the International Conference on Automated Deduction (CADE-16), pages 202–206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.
Andrew M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer and Andrew M. Pitts, editors, Semantics and Logics of Computation. Cambridge University Press, 1995. Based on lectures given at the CLICS-II Summer School on Semantics and Logics of Computation, Isaac Newton Institute for Mathematical Sciences, Cambridge UK, September 1995.
Gordon D. Plotkin. A powerdomain construction. SIAM Journal of Computing, 5(3):452–487, September 1976.
Gordon D. Plotkin. A structural approach to operational semantics. Technical report, Computer Science Department, Aarhus University, 1981.
Gordon D. Plotkin. An operational semantics for CSP. Technical report, University of Edinburgh, Department of Computer Science, 1982.
Jean-Claude Raoult and Jean Vuillemin. Operational and semantic equivalence between recursive programs. JACM, 27(4):772–796, October 1980.
Jonathan Rees, William Clinger, H. Abelson, N. I. Adams IV, D. Bartley, G. Brooks, R. K. Dybvig, D. P. Friedman, R. Halstead, C. Hanson, C. T. Haynes, E. Kohlbecker, D. Oxley, K. M. Pitman, G. J. Rozas, G. J. Sussman, and M. Wand. Revised4 report on the algorithmic language Scheme. Technical Report AI Memo 848b, MIT Press, 1992.
David Sands. A naïve time analysis and its theory of cost equivalence. Journal of Logic and Computation, 5(4), 1995.
Michael B. Smyth. Powerdomains. In the Mathematical Foundations of Computer Science Symposium, volume 45 of Lecture Notes in Computer Science, pages 537–543. Springer-Verlag, 1976.
Joseph E. Stoy. Some mathematical aspects of functional programming. In John Darlington, Peter Henderson, and David A. Turner, editors, Functional Programming and its Applications, pages 217–252. Cambridge University Press, 1982.
Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, 1999. Available from [77].
Walid Taha, editor. Semantics, Applications, and Implementation of Program Generation, volume 1924 of Lecture Notes in Computer Science, Montréal, 2000. Springer-Verlag.
Walid Taha and Tim Sheard. Multi-stage programming with explicit annotations. In Proceedings of the Symposium on Partial Evaluation and Semantic-Based Program Manipulation (PEPM), pages 203–217, Amsterdam, 1997. ACM Press.
Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. In A. Scedrov, editor, Proceedings of the 1992Logics in Computer Science Conference, pages 162–173. IEEE, 1992.
Alastair Telford and David Turner. EnsuringStreams Flow. In Michael Johnson, editor, Algebraic Methodology and Software Technology, 6th International Conference, AMAST’ 97, Sydney Australia, December 1997, volume 1349 of Lecture Notes in Computer Science, pages 509–523. AMAST, Springer-Verlag, December 1997.
Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1 February 1997.
David A. Turner. Functional programs as executable specifications. Philosophical Transactions of the Royal Society of London, A312:363–388, 1984.
Philip Wadler. The essence of functional programming. In the Symposium on Principles of Programming Languages (POPL’ 92), pages 1–14. ACM, January 1992.
Philip Wadler. The marriage of effects and monads. In the International Conference on Functional Programming (ICFP’ 98), volume 34(1) of ACM SIGPLAN Notices, pages 63–74. ACM, June 1999.
Zhanyong Wan and Paul Hudak. Functional reactive programmingfrom first principles. In the Symposium on Programming Language Design and Implementation (PLDI’ 00). ACM, 2000.
Zhanyong W an, Walid Taha, and Paul Hudak. Real-time FRP. In the International Conference on Functional Programming (ICFP’ 01), Florence, Italy, September 2001.
Hongwei Xi. Upper bounds for standardizations and an application. Journal of Symbolic Logic, 64(1):291–303, March 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Taha, W., Hudak, P., Wan, Z. (2001). Directions in Functional Programming for Real(-Time) Applications. In: Henzinger, T.A., Kirsch, C.M. (eds) Embedded Software. EMSOFT 2001. Lecture Notes in Computer Science, vol 2211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45449-7_13
Download citation
DOI: https://doi.org/10.1007/3-540-45449-7_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42673-8
Online ISBN: 978-3-540-45449-6
eBook Packages: Springer Book Archive