Towards machine-verified proofs for I/O

Abstract. In functional languages, the shape of the external world af-fects both our understanding of I/O and how we would wish to have I/O expressed. This paper takes the first tentative steps at examining the consequences of using an explicit model of the external world-state when reasoning (using tool-support) about the behaviour of lazy func-tional programs. We construct a file-system model and develop a monadic language which lets us structure I/O. Two proofs are then performed re-garding the observable effect of real-world functional I/O, and it is shown how properties of the file-system lend themselves naturally to the mod-elling of concurrent behaviour on a single, global state. All proofs in this paper were machine-verified using the Sparkle proof-assistant