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 μ?)
I uploaded a half-dozen pages of notes on how to do "full" linear logic in labelled style to my drafts page. The big surprise is that additive falsehood ("0") breaks spectacularly. I'm also missing the exponential, but I've sketched that out enough in other places that I'm pretty sure it works.
Anyway big thanks are owed to the ultra-slick higher-order completeness lemma that came out of Frank and
simrob's recent work.*coinductive types also wish you a happy valentine's day. Γ ⊢ να.(♥ + α), I guess?