Skip to main content
SpringerLink
Log in

The algebra of functional programs: Function level reasoning, linear equations, and extended definitions

  • Invited Lectures
  • Conference paper
  • First Online:
Formalization of Programming Concepts (ICFPC 1981)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 107))

Included in the following conference series:

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ARBIB, M.A. and MANES, E.G. The pattern-of-calls expansion is the canonical fixpoint for recursive definitions. Tech. Rep. Math. and Statistics, Univ. of Mass., Amherst, Mass., Jan. 1979.

    Google Scholar 

  2. ARBIB, M.A. and MANES, E.G. Partially additive categories and flow-diagram semantics. J. Algebra 62, 1, Jan. 1980.

    Google Scholar 

  3. ARNOLD, M. (Private communication), May, 1980.

    Google Scholar 

  4. BURSTALL, R.M. and DARLINGTON, J. A transformation system for developing recursive programs. JACM 24, 1, Jan. 1977.

    Google Scholar 

  5. BURSTALL, R.M. and GOGUEN, J.A. Putting theories together to make specifications. Proc. International Joint Conference on Artificial Intelligence, Cambridge, Mass. 1977.

    Google Scholar 

  6. BURSTALL, R.M. and GOGUEN, J.A. The semantics of Clear, a specification language. Proc. 1979 Copenhagen Winter School on Abstract Software Specifications, Copenhagen. Feb. 1980.

    Google Scholar 

  7. BOHM, C. and JACOPINI, G. Flow diagrams, Turing machines, and languages with only two formation rules. CACM 9, 5, May 1966.

    Google Scholar 

  8. BOYER, R.S. and MOORE, J.S. A computational logic. Academic Press, New York, 1979.

    Google Scholar 

  9. BACKUS, J. Programming language semantics and closed applicative languages. Conf. Record, ACM Symp. on Principles of Programming Languages, Boston, Mass. Oct. 1973.

    Google Scholar 

  10. BACKUS, J. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. CACM 21, 8, Aug. 1978.

    Google Scholar 

  11. BACKUS, J. On extending the concept of "program" and solving linear functional equations. Draft paper distributed at Summer Workshop on Programming Methodology, Univ. of Calif, Santa Cruz, Aug. 1979.

    Google Scholar 

  12. BURGE, W.H. Even more structured programming. Tech. Rept. RC4604 IBM Thos. J. Watson Research Center, Yorktown Hts, NY, Oct. 1973.

    Google Scholar 

  13. BURSTALL, R.M. Proving properties of programs by structural induction. Computer J. 12, 1, Feb. 1969.

    Google Scholar 

  14. CADIOU, J.M. Recursive definitions of partial functions and their computations. PhD Thesis, Computer Science Dept., Stanford Univ., Stanford, Calif. Mar. 1972.

    Google Scholar 

  15. CHURCH, A. The calculi of lambda-conversion. Princeton Univ. Press, Princeton, NJ. 1941.

    Google Scholar 

  16. CURRY, H.B. and FEYS, R. Combinatory logic. North-Holland, Amsterdam, 1958 (second printing 1968)

    Google Scholar 

  17. deBAKKER, J.W. and SCOTT, D. A theory of programs. (Unpublished memo.) Aug. 1969.

    Google Scholar 

  18. GUTTAG, J.V., HOROWITZ, E., and MUSSER, D.R. Abstract data types and software validation. CACM 21, 12, Dec. 1978.

    Google Scholar 

  19. GOGUEN, J.A., THATCHER, J.W., WAGNER, E.G., and WRIGHT, J.B. Initial algebra semantics and continuous algebras. JACM 24, 1, Jan. 1977.

    Google Scholar 

  20. HOARE, C.A.R. An axiomatic basis for computer programming. CACM 12, 10, Oct. 1969.

    Google Scholar 

  21. KLEENE, S.C. Introduction to metamathematics. D. van Nostrand, Princeton, NJ 1952.

    Google Scholar 

  22. LANDIN, P.J. The mechanical evaluation of expressions. Computer J. 6, 4, 1964.

    Google Scholar 

  23. MANNA, Z., NESS, S., and VUILLEMIN, J. Inductive methods for proving properties of programs. CACM 16, 8, Aug. 1973.

    Google Scholar 

  24. MANNA, Z. and PNUELI, A. Formalization of properties of functional programs. JACM 17, 3, July 1970.

    Google Scholar 

  25. MARTIN, J.J. Typed functional programming systems. Tech. Rept. Comp. Sci. Dept., Virginia Polytechnic Inst. and State Univ. Blacksburg, VA. 1980.

    Google Scholar 

  26. MCCARTHY, J. A basis for a mathematical theory of computation. (in) Computer Programming and Formal Systems, P. Braffort and D. Hirshberg (eds.), North Holland, Amsterdam, 1963.

    Google Scholar 

  27. MILNER, R. Models of LCF. Mathematical Centre Tracts 82, Univ. of Edinburgh, Edinburgh, 1976.

    Google Scholar 

  28. MORRIS, J.H. Jr. Another recursion induction principle. CACM 14, 5, May 1971.

    Google Scholar 

  29. MUSSER, D.R. Convergent sets of rewrite rules for abstract data types. Tech. Rept., Univ. of So. Calif. Information Scis. Inst., Marina del Rey, Calif. Dec. 1978.

    Google Scholar 

  30. NAUR, P. Proof of algorithms by general snapshots. BIT 6, 1966.

    Google Scholar 

  31. PARK, D. Fixpoint induction and proofs of program properties. (in) Machine Intelligence 5, B. Meltzer and D. Michie, (eds.)

    Google Scholar 

  32. RAYMOND, F.H. Note sur l'algebre des fonctions. R.A.I.R.O. R-3, Dec. 1975.

    Google Scholar 

  33. RAYMOND, F.H. Note sur la suppression des étiquettes en programmation. R.A.I.R.O. 11, 1, 1977.

    Google Scholar 

  34. SCOTT, D. Outline of a mathematical theory of computation. Proc. Fourth Annual Princeton Conf. on Information Sciences and Systems, Princeton Univ. 1970.

    Google Scholar 

  35. TURNER, D.A. SASL language manual. Tech. Rept., Univ. of Kent, Canterbury, Aug. 1979.

    Google Scholar 

  36. TURNER, D.A. A new implementation technique for applicative languages. Software—Practice and Experience 9, 1979.

    Google Scholar 

  37. WALKER, S.A. and STRONG, H.R. Characterizations of flowchartable recursions. J. Computer and System Sciences 7, 4, Aug. 1973.

    Google Scholar 

  38. WILLIAMS, J. H. On the development of the algebra of functional programs. Tech. Rept. RJ2983, IBM Research Lab., San Jose, Calif. Oct. 1980.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IBM Research Laboratory, 5600 Cottle Road, 95193, San Jose, California, USA

    John Backus

Authors
  1. John Backus
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. Díaz I. Ramos

Rights and permissions

Reprints and permissions

Copyright information

© 1981 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Backus, J. (1981). The algebra of functional programs: Function level reasoning, linear equations, and extended definitions. In: Díaz, J., Ramos, I. (eds) Formalization of Programming Concepts. ICFPC 1981. Lecture Notes in Computer Science, vol 107. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10699-5_91

Download citation

  • DOI: https://doi.org/10.1007/3-540-10699-5_91

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-10699-9

  • Online ISBN: 978-3-540-38654-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation