What is the folk model of linear logic?

Question

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?

Answer 1

It seems to me that the direction you should consider looking in revolves around game semantics for general references and the related semantics for linear logic, such as those based on Conway games. An algebraic account of references in game semantics by Paul-André Melliès and Nicolas Tabareau is probably the best place to start. In this paper linear logic is relaxed to so-called tensor logic to get things to work, so it is not quite the setting you want. But they do rely on Conway games, so there is certainly a connection with models of linear logic. They also do not really exploit linearity as in linear types, but the machinery is there to do so if you want to, I believe.

The work of Jim Laird (such as A Game Semantics of Names and Pointers) and Guy McCusker may also contribute to your quest. The recent interesting thesis Game semantics for an object-oriented language by Nicholas Wolverson pushes these ideas further in an OO setting. He considers in detail linear threading, only one operation active at a time, and describes how to add linear classes. Both rely on linear typing. Again, however, the underlying model is not strictly a model of linear logic, but it's close.

Answer 2

(Gosh, Neel, that was a tough question.)

The "folk model" of linear logic is definitely the coherent spaces model, discussed in Girard's Linear Logic paper (and also in "Proofs and Types"). This is not degenerate in the sense you describe.

Whether this semantics throws any light on how a linear functional language can be implemented, I am not sure. When you are talking about allocation, reading and linear update, you are indeed talking about the implementation. So, perhaps, your question might be formulated as, "how do I prove correct the implementation of a linear functional language that uses state-update?" I don't know the answer to that, but I think it must exist in the papers that propose linear update implementations.