A Language for Reasoning about Concurrent Functional I/O

Malcolm Dowse, Andrew Butterfield and Marko van Eekelen

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.

All properties were machine-verified using the Sparkle proof-assistant and using Core-Clean as a meta-language.