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?