Reasoning about I/O in Functional Programs

• 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 

• Bird, R., de Moor, O.: Algebra of Programming. Series in Computer Science. Prentice Hall International, London (1987)

  MATH  Google Scholar 

• 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)

  Chapter  Google Scholar 

• 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)

  MATH  Google Scholar 

• 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 

• Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science 37(1), 77–121 (1985)

  Article  MathSciNet  MATH  Google Scholar 

• Barendsen, E., Smetsers, S.: Uniqueness Typing for Functional Languages with Graph Rewriting Semantics. Mathematical Structures in Computer Science 6(6), 579–612 (1996)

  MathSciNet  MATH  Google Scholar 

• 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)

  Chapter  Google Scholar 

• Bird, R., Wadler, P.: Introduction to Functional Programming. Series in Computer Science. Prentice Hall International, London (1988)

  Google Scholar 

• 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 

• VDM Standards Committee. VDM Specification Language — Proto-Standard. Technical report, VDM Standards Committee (1992)

  Google Scholar 

• Davie, A.J.T.: An Introduction to Functional Programming Systems using Haskell. Cambridge Computer Science Texts. Cambridge University Press (1992)

  Google Scholar 

• 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 

• 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/

• 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)

  Chapter  Google Scholar 

• 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 

• 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)

  Chapter  Google Scholar 

• 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)

  Chapter  Google Scholar 

• Espinosa, D.A.: Semantic Lego. PhD thesis, University of Columbia (1995)

  Google Scholar 

• Gordon, A.: Functional Programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press (1994)

  Google Scholar 

• Henson, M.C.: Elements of Functional Languages. Computer Science Texts. Blackwell Scientific Publications (1987)

  Google Scholar 

• Hennessy, M.: The Semantics of Programming Languages: An elementary introduction using Structured Operational Semantics. Wiley (1990)

  Google Scholar 

• 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)

  Chapter  Google Scholar 

• 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 

• Hoare, C.A.R.: Communicating Sequential Processes. Intl. Series in Computer Science. Prentice Hall (1990)

  Google Scholar 

• Jones, C.B.: Systematic Software Development using VDM. Series in Computer Science. Prentice Hall (1989)

  Google Scholar 

• 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)

  Chapter  Google Scholar 

• 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 

• 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 

• 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 

• McKinna, J.: Why dependent types matter. In: Gregory Morrisett, J., Peyton Jones, S.L. (eds.) POPL, p. 1. ACM (2006)

  Google Scholar 

• Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

  Book  MATH  Google Scholar 

• Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)

  Google Scholar 

• Oliveira, M., Cavalcanti, A., Woodcock, J.: A denotational semantics for circus. In: REFINE 2006, pp. 1–16. ENTCS (2006)

  Google Scholar 

• Peyton-Jones, S.L.: The Implementation of Functional Programming Languages. Series in Computer Science. Prentice Hall International, London (1987)

  MATH  Google Scholar 

• 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 2000

  Google Scholar 

• Plotkin, G.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Department of Computer Science, Aarhus University, Denmark (1981)

  Google Scholar 

• Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Boston (1986)

  Google Scholar 

• Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Series in Computer Science. Prentice Hall (1992)

  Google Scholar 

• Stoy, J.E.: Denotational Semantics: The Scott-Strachey approach to programming language theory. MIT Press, Cambridge (1977)

  MATH  Google Scholar 

• 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 

Download references