This dissertation presents a pure functional language called Curio. This language is unusual in possessing a rigorous yet general semantics for I/O which permits both formal proofs and a fine-tuned approach to concurrency. ...