Formal Methods within a Totally Functional Approach to Programming

  • Paul A. Bailes
  • Colin J. M. Kemp
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2757)


Taking functional programming to its extremities in search of simplicity still requires integration with other development (e.g. formal) methods. Induction is the key to deriving and verifying functional programs, but can be simplified through packaging proofs with functions, particularly “folds”, on data (structures). “Totally Functional Programming” avoids the complexities of interpretation by directly representing data (structures) as “platonic combinators” – the functions characteristic to the data. The link between the two simplifications is that platonic combinators are a kind of partially-applied fold, which means that platonic combinators inherit fold-theoretic properties, but with some apparent simplifications due to the platonic combinator representation. However, despite observable behaviour within functional programming that suggests that TFP is widely-applicable, significant work remains before TFP as such could be widely adopted.


Formal Method Functional Approach Functional Programming Functional Language Language Extension 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Turner, D.A.: Miranda - a non-strict functional language with polymorphic types. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 1–16. Springer, Heidelberg (1985)Google Scholar
  2. 2.
    Hughes, J.: Why Functional Programming Matters. The Computer Journal 32(2), 98–107 (1989)CrossRefGoogle Scholar
  3. 3.
    Bird, R.: Introduction to Functional Programming. Prentice-Hall, Englewood Cliffs (2000)Google Scholar
  4. 4.
  5. 5.
    Hutton, G.: A Tutorial on the Universality and Expressiveness of Fold. Journal of Functional Programming 9(4), 355–372 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Barendregt, H.P.: The Lambda Calculus - Its Syntax and Semantics. North-Holland, Amsterdam (1984)zbMATHGoogle Scholar
  7. 7.
    Aho, A.V., Ullman, J.D.: The Theory of Parsing, Translation and Compiling. Prentice-Hall, Englewood Cliffs (1972)Google Scholar
  8. 8.
    Hutton, G.: Parsing Using Combinators. In: Proc. Glasgow Workshop on Functional Programming. Springer, Heidelberg (1989)Google Scholar
  9. 9.
    Boehm, H., Cartwright, R.: Exact Real Arithmetic: Formulating Real Numbers as, Functions. In: Turner, D.A. (ed.) Research Topics in Functional Programming, pp. 43–64. Addison-Wesley, Reading (1990)Google Scholar
  10. 10.
    Sheard, T., Fougaras, L.: A fold for all seasons. In: Proc. ACM Conference on Functional Programming and Computer Architecture. Springer, Heidelberg (1993)Google Scholar
  11. 11.
    Milner, R.: A Theory of Type Polymorphism in Programming. J. Comp. Syst. Scs. 17, 348–375 (1977)CrossRefMathSciNetGoogle Scholar
  12. 12.
    Reynolds, J.C.: Three approaches to type structure. In: Nivat, M., Floyd, C., Thatcher, J., Ehrig, H. (eds.) CAAP 1985 and TAPSOFT 1985. LNCS, vol. 185. Springer, Heidelberg (1985)Google Scholar
  13. 13.
    Jones, M.P.: First-class Polymorphism with Type Inference. In: Proc. 24th ACM Symposium on Principles of Programming Languages (1997)Google Scholar
  14. 14.
    Peyton Jones, S.: The Implementation of Functional Programming Languages. Prentice-Hall International, Hemel Hempstead (1987)zbMATHGoogle Scholar
  15. 15.
    Royer, J.S., Case, J.: Subrecursive Programming Systems: Complexity & Succintness. Birkhauser, Basel (1994)Google Scholar
  16. 16.
    Turner, D.A.: Elementary Strong Functional Programming. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol. 1022, pp. 1–13. Springer, Heidelberg (1995)Google Scholar
  17. 17.
    Backus, J.: Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. Comm. ACM 21(8), 613–641 (1978)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Bailes, P.A.: The Programmer as Language Designer (Towards a Unified Theory of Programming and Language Design). In: Proceedings of the 1986 Australian Software Engineering Conference, Canberra, pp. 14–18 (1986)Google Scholar
  19. 19.
    Bailes, P.A., Chorvat, T., Peake, I.: A Formal Basis for the Perception of Programming as a Language Design Activity. In: Proc. 1994 International Conference on Computing and Information, Peterborough (1994)Google Scholar
  20. 20.
    Plotkin, G.D.: PCF Considered as a Programming Language. Theoretical Computer Science 5, 223–255 (1977)CrossRefMathSciNetGoogle Scholar
  21. 21.
    Chikofsky, E., Cross II, J.H.: Reverse engineering and design recovery: a taxonomy. IEEE Software, 13–17 (January 1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Paul A. Bailes
    • 1
  • Colin J. M. Kemp
    • 1
  1. 1.School of Information Technology and Electrical EngineeringThe University of QueenslandAustralia

Personalised recommendations