neelk pointed me to A λ-calculus for resource separation by Bob Atkey. He also talked a bit about what Carsten Varming did last summer. Carsten tried to explain it to me in the elevator the other day, but I didn't get it then. It has something to do with a constructive development in Coq of domain theory. The cute thing about it is the fact that, morally, the nontermination monad isn't (as I sort of passively thought it was) the same as the exception monad λX.X+1, which provides a single other computational alternative to returning a value of type X. How you should think of it is the type operator λX.να.X+α, which given a type X returns the coinductive stream type να.X+α, which you can read as "eventually maybe X". All you can do with the stream is ask it to unroll one step, at which point you find either the long-sought X you were hoping against hope to find, or again να.X+α telling you to keep waiting another day*.
Anyway I thought this was a nice and utterly syntactically simple way of capturing the fact that nontermination is a computational process and not an alternative value. It is in fact a monad. (good exercise: what is its μ?)