Advertisement

Reasoning About Deterministic Concurrent Functional I/O

  • Malcolm Dowse
  • Andrew Butterfield
  • Marko van Eekelen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3474)

Abstract

This paper develops a language for reasoning about concurrent functional I/O. We assume that the API is specified as state-transformers on a single world state. We then prove that under certain conditions evaluation in this language is deterministic, and give some examples. All properties were machine-verified using the Sparkle proof-assistant and using Core-Clean as a meta-language.

Keywords

Global State Operational Semantic Reduction Order Functional Language Algebraic Type 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Barendsen, E., Smetsers, S.: Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science 6(6), 579–612 (1996)zbMATHMathSciNetGoogle Scholar
  2. 2.
    Butterfield, A., Strong, G.: Proving correctness of programs with I/O – a paradigm comparison. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol. 2312, pp. 72–87. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Carter, D.: Deterministic concurrency. Master’s thesis, Department of Computer Science, University of Bristol (September 1994)Google Scholar
  4. 4.
    de Mol, M., van Eekelen, M., Plasmeijer, R.: Sparkle: A functional theorem prover. In: Arts, T., Mohnen, M. (eds.) IFL 2001. LNCS, vol. 2312, p. 55. Springer, Heidelberg (2002)Google Scholar
  5. 5.
    Dowse, M., Butterfield, A., van Eekelen, M., de Mol, M., Plasmeijer, R.: Towards machine verified proofs for I/O. Technical Report NIII-R0415, University of Nijmegen (April 2004)Google Scholar
  6. 6.
    Dowse, M., Strong, G., Butterfield, A.: 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
  7. 7.
    Gordon, A.D.: An operational semantics for I/O in a lazy functional language. In: Proceedings of the Conference on Functional Programming Languages and Computer Architecture, New York, USA, pp. 136–145. ACM Press, New York (1993)CrossRefGoogle Scholar
  8. 8.
    Hall, C., Hammond, K.: A dynamic semantics for haskell (draft) (May 20, 1993)Google Scholar
  9. 9.
    Holyer, I., Spiliopoulou, E.: Concurrent monadic interfacing. In: Hammond, K., Davie, T., Clack, C. (eds.) IFL 1998. LNCS, vol. 1595, pp. 73–89. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Hudak, P., Sundaresh, R.S.: On the expressiveness of purely functional I/O systems. Technical report, Yale University (1989)Google Scholar
  11. 11.
    Jones, M.P., Duponcheel, L.: Composing monads. Technical report, Yale University (December 1993)Google Scholar
  12. 12.
    Peyton Jones, S., Gordon, A., Finne, S.: Concurrent Haskell. In: ACM (ed.) POPL 1996: Florida, January 21–24, 1996, New York, USA, pp. 295–308. ACM Press, New York (1996)Google Scholar
  13. 13.
    Peyton Jones, S., Wadler, P.: Imperative functional programming. In: ACM (ed.) POPL 1993: Charleston, January 10–13, 1993, New York, USA, pp. 71–84. ACM Press, New York (1993)Google Scholar
  14. 14.
    Plasmeijer, R., van Eekelen, M.: Concurrent clean version 2.0 language report (December 2001), http://www.cs.kun.nl/~clean/

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Malcolm Dowse
    • 1
  • Andrew Butterfield
    • 1
  • Marko van Eekelen
    • 2
  1. 1.Trinity College DublinIreland
  2. 2.University of NijmegenThe Netherlands

Personalised recommendations