Imprecise exceptions, co-inductively

In a recent paper, Peyton Jones et al proposed a design for imprecise exceptions in the lazy functional programming language Haskell. The main contribution of the design was that it allowed the language to continue to enjoy its current rich algebra of transformations. However, the denotational semantics used to formalise the design does not combine easily with other extensions, most notably that of concurrency. We present an alternative semantics for a lazy functional language with imprecise exceptions which is entirely operational in nature, and combines well with other extensions, such as I/O and concurrency. The semantics is based upon a convergence relation, which describes evaluation, and an exceptional convergence relation, which describes the raising of exceptions. Convergence and exceptional convergence lead naturally to a simple notion of refinement, where a term $M$ is refined by $N$ whenever they have identical convergent behaviour, and any exception raised by $N$ can also be raised by $M$. We are able to validate many call-by-name equivalences and standard program transformations, including the ubiquitous strictness transformation.