Advertisement

Reasoning about I/O in Functional Programs

  • Andrew Butterfield
Chapter
  • 558 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7241)

Abstract

We look at formalisms for reasoning about the effects of I/O in pure functional programs, covering both the monadic I/O of Haskell and the uniqueness-based framework used by Clean. The material will cover comparative studies of I/O reasoning for Haskell, Clean and a C-like language, as well as describing the formal infrastructure needed and tool support available to do such reasoning.

Keywords

Operational Semantic Label Transition System Proof Obligation Denotational Semantic Program Text 
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.
This is a preview of subscription content, log in to check access.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.-R., Lee, M.K.O., Neilson, D.S., Scharbach, P.N., Sørensen, I.H.: The B Method. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 398–405. Springer, Heidelberg (1991)Google Scholar
  2. Bird, R., de Moor, O.: Algebra of Programming. Series in Computer Science. Prentice Hall International, London (1987)zbMATHGoogle Scholar
  3. Butterfield, A., Dowse, M., Strong, G.: Proving Make Correct: I/O Proofs in Haskell and Clean. In: Peña, R., Arts, T. (eds.) IFL 2002. LNCS, vol. 2670, pp. 68–83. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. Banâtre, J.-P., Jones, S.B., Le Métayer, D.: Prospects for Functional Programming in Software Engineering. ESPRIT Research Reports, Project 302, vol. 1. Springer, Berlin (1991)zbMATHGoogle Scholar
  5. Bjørner, D.: Trusted computing systems: the procos experience. In: Proceedings of the 14th International Conference on Software Engineering, ICSE 1992, pp. 15–34. ACM, New York (1992)Google Scholar
  6. Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science 37(1), 77–121 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  7. Barendsen, E., Smetsers, S.: Uniqueness Typing for Functional Languages with Graph Rewriting Semantics. Mathematical Structures in Computer Science 6(6), 579–612 (1996)MathSciNetzbMATHGoogle Scholar
  8. Butterfield, A., Strong, G.: Proving Correctness of Programs with IO – A Paradigm Comparison. In: Arts, T., Mohnen, M. (eds.) IFL 2001. LNCS, vol. 2312, pp. 72–87. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. Bird, R., Wadler, P.: Introduction to Functional Programming. Series in Computer Science. Prentice Hall International, London (1988)Google Scholar
  10. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: Conference Record of the Nineteenth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, January 19-22, pp. 343–354. ACM Press (1992)Google Scholar
  11. VDM Standards Committee. VDM Specification Language — Proto-Standard. Technical report, VDM Standards Committee (1992)Google Scholar
  12. Davie, A.J.T.: An Introduction to Functional Programming Systems using Haskell. Cambridge Computer Science Texts. Cambridge University Press (1992)Google Scholar
  13. Dowse, M., Butterfield, A.: Modelling deterministic concurrent I/O. In: Reppy, J.H., Lawall, J.L. (eds.) Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, pp. 148–159. ACM (2006)Google Scholar
  14. Dowse, M., Butterfield, A., van Eekelen, M., de Mol, M.: Towards Machine Verified Proofs for I/O. Technical Report NIII-R0415, nijmeegs institut voor informatica en informatiekunde (2004), http://www.cs.kun.nl/research/reports/
  15. Déharbe, D., Galvão, S., Moreira, A.M.: Formalizing FreeRTOS: First Steps. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol. 5902, pp. 101–117. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. de Mol, M.: Reasoning about Functional Programs: Sparkle, a proof assistant for Clean. PhD thesis, Institute for Programming research and Algorithmics, Radboud University Nijmegen (2009)Google Scholar
  17. de Mol, M., van Eekelen, M., Plasmeijer, R.: Theorem Proving for Functional Programmers. In: Arts, T., Mohnen, M. (eds.) IFL 2001. LNCS, vol. 2312, pp. 55–71. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  18. de Mol, M., van Eekelen, M., Plasmeijer, R.: Proving Properties of Lazy Functional Programs with Sparkle. In: Horváth, Z., Plasmeijer, R., Soós, A., Zsók, V. (eds.) CEFP 2007. LNCS, vol. 5161, pp. 41–86. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  19. Espinosa, D.A.: Semantic Lego. PhD thesis, University of Columbia (1995)Google Scholar
  20. Gordon, A.: Functional Programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press (1994)Google Scholar
  21. Henson, M.C.: Elements of Functional Languages. Computer Science Texts. Blackwell Scientific Publications (1987)Google Scholar
  22. Hennessy, M.: The Semantics of Programming Languages: An elementary introduction using Structured Operational Semantics. Wiley (1990)Google Scholar
  23. Holzmann, G.J., Joshi, R.: Reliable Software Systems Design: Defect Prevention, Detection, and Containment. In: Meyer, B., Woodcock, J. (eds.) Verified Software. LNCS, vol. 4171, pp. 237–244. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  24. Harrison, W.L., Kamin, S.N.: Modular compilers based on monad transformers. In: Proceedings of the IEEE International Conference on Computer Languages, pp. 122–131. Society Press (1998)Google Scholar
  25. Hoare, C.A.R.: Communicating Sequential Processes. Intl. Series in Computer Science. Prentice Hall (1990)Google Scholar
  26. Jones, C.B.: Systematic Software Development using VDM. Series in Computer Science. Prentice Hall (1989)Google Scholar
  27. Kahn, G.: Natural Semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  28. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: Sel4: Formal verification of an os kernel. In: ACM Symposium on Operating Systems Principles, pp. 207–220. ACM (2009)Google Scholar
  29. Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: Proceedings of the 22nd ACM Symposium on Principles of Programming Languages. ACM Press (1995)Google Scholar
  30. Macan Airchinnigh, M.: Tutorial Lecture Notes on the Irish School of the VDM. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 141–237. Springer, Heidelberg (1991)Google Scholar
  31. McKinna, J.: Why dependent types matter. In: Gregory Morrisett, J., Peyton Jones, S.L. (eds.) POPL, p. 1. ACM (2006)Google Scholar
  32. Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)CrossRefzbMATHGoogle Scholar
  33. Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)Google Scholar
  34. Oliveira, M., Cavalcanti, A., Woodcock, J.: A denotational semantics for circus. In: REFINE 2006, pp. 1–16. ENTCS (2006)Google Scholar
  35. Peyton-Jones, S.L.: The Implementation of Functional Programming Languages. Series in Computer Science. Prentice Hall International, London (1987)zbMATHGoogle Scholar
  36. Peyton-Jones, S.L.: Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in haskell. In: Hoare, C.A.R., Broy, M., Steinbrueggen, R. (eds.) Engineering Theories of Software Construction. NATO ASI Series, pp. 47–96. IOS Press (2001); Marktoberdorf Summer School 2000Google Scholar
  37. Plotkin, G.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Department of Computer Science, Aarhus University, Denmark (1981)Google Scholar
  38. Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Boston (1986)Google Scholar
  39. Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Series in Computer Science. Prentice Hall (1992)Google Scholar
  40. Stoy, J.E.: Denotational Semantics: The Scott-Strachey approach to programming language theory. MIT Press, Cambridge (1977)zbMATHGoogle Scholar
  41. Verhulst, E., Boute, R.T., Faria, J.M.S., Sputh, B.H.C., Mezhuyev, V.: Formal Development of a Network-Centric RTOS. Springer (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Andrew Butterfield
    • 1
  1. 1.Trinity College, University of DublinIreland

Personalised recommendations

Cite chapter

Buy options