Probably the most common application of linear types in PL is to use them to give languages which control aliasing (i.e., a linear value has a single pointer to it, more or less).
But there's a slight mismatch between this usage and typical denotational models of linear logic. IIRC, Benton showed that if a Cartesian closed category has a strong commutative monad, then its category of algebras will be symmetric monoidal closed (ie, a model of linear logic). But this theorem doesn't apply to the alias-control usage, since the state monad is not commutative. And indeed, in the past few years Simpson and his coworkers have given calculi for general strong monads, which are not term calculi for linear logic.
So my question is, what is the denotational semantics of linear languages with state? Is there a non-degenerate (ie, tensor is not a Cartesian product) symmetric monoidal closed category in which allocation, reading, and linear update can be modeled?