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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Barendsen, E., Smetsers, S.: Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science 6(6), 579–612 (1996)
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)
Carter, D.: Deterministic concurrency. Master’s thesis, Department of Computer Science, University of Bristol (September 1994)
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)
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)
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)
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)
Hall, C., Hammond, K.: A dynamic semantics for haskell (draft) (May 20, 1993)
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)
Hudak, P., Sundaresh, R.S.: On the expressiveness of purely functional I/O systems. Technical report, Yale University (1989)
Jones, M.P., Duponcheel, L.: Composing monads. Technical report, Yale University (December 1993)
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)
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)
Plasmeijer, R., van Eekelen, M.: Concurrent clean version 2.0 language report (December 2001), http://www.cs.kun.nl/~clean/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dowse, M., Butterfield, A., van Eekelen, M. (2005). Reasoning About Deterministic Concurrent Functional I/O. In: Grelck, C., Huch, F., Michaelson, G.J., Trinder, P. (eds) Implementation and Application of Functional Languages. IFL 2004. Lecture Notes in Computer Science, vol 3474. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11431664_11
Download citation
DOI: https://doi.org/10.1007/11431664_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26094-3
Online ISBN: 978-3-540-32038-8
eBook Packages: Computer ScienceComputer Science (R0)