Proving Make Correct: I/O Proofs in Haskell and Clean. - Malcolm Dowse; Glenn Strong; Andrew Butterfield (IFL, 2002)

Reasoning About Deterministic Concurrent Functional I/O. - Malcolm Dowse; Andrew Butterfield; Marko C. J. D. van Eekelen (IFL, 2004)

Modelling deterministic concurrent I/O. - Malcolm Dowse; Andrew Butterfield (ICFP, 2006)

A Semantic framework for deterministic functional input/output - Malcolm Dowse (2006)