A Language for Reasoning about Concurrent Functional I/O
Malcolm Dowse, Andrew Butterfield and Marko van Eekelen
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.