<p>It seems to me that the direction you should consider looking in revolves around <em>game semantics</em> for general references and the related semantics for linear logic,
such as those based on <a href="http://www.pps.jussieu.fr/~mellies/papers/ag3-ctcs.pdf">Conway games</a>.  <a href="http://www.pps.jussieu.fr/~mellies/papers/mfps2009-references.pdf">An algebraic account of references in game semantics</a> 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.</p>

<p>The work of <a href="http://www.cogs.susx.ac.uk/users/jiml">Jim Laird</a> (such as <a href="http://www.cogs.susx.ac.uk/users/jiml/pointers3.pdf">A Game Semantics of Names and Pointers</a>) and <a href="http://www.cs.bath.ac.uk/~gam23/papers.html">Guy McCusker</a> may also contribute to your quest. The recent interesting thesis <a href="http://homepages.inf.ed.ac.uk/jrl/Eriskay/wolverson-thesis-final.pdf">Game semantics for an object-oriented language</a> by Nicholas Wolverson pushes these ideas further in an OO setting. He considers in detail <em>linear threading</em>, only one operation active at a time, and describes how to add <em>linear classes</em>. Both rely on linear typing. 
Again, however, the underlying model is not strictly a model of linear logic, but it's close.</p>

CC BY-SA 2.5
2010-11-15T14:04:42.350Z
Just curious Neel. Was this of any use to you, or did you know about all of this stuff already?
Dave Clarke
CC BY-SA 2.5
2010-11-17T11:36:48.450Z
I know this stuff (but not well), but game semantics is a lot more sophisticated than what I'm looking for. Most people have an intuition for linear state which is not far from the old-fashioned Strachey view of an imperative computation as an element of a monadic type $T(A) = S \to A \times S$, and I was hoping there was a model of linear state which would resemble that. Basically, I was hoping there was something you could show a first-year grad student without terrifying them. :)
Neel Krishnaswami
CC BY-SA 2.5
2010-11-17T11:49:59.747Z
Maybe Uday Reddy's
Global state considered unnecessary: An introduction to object-based semantics, J. Lisp and Symbolic Computation, 9(1996):7-76.
Dave Clarke
CC BY-SA 2.5
2010-11-17T13:52:45.377Z
I'm reading that now, actually!
Neel Krishnaswami
CC BY-SA 2.5
2010-11-11T11:52:33.203Z
2010-11-11T11:52:33.203Z
Dave Clarke
<p>(Gosh, Neel, that was a tough question.)</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2012-02-29T11:21:00.163Z
Actually, it's *too easy* to prove the correctness of implementations of linear state -- linearity is such a strong structural constraint that you hardly need any semantics to do these proofs. As a result, I don't know a simple denotational semantics of linear state. The two closest things to what I want are your work on object-based semantics, and the "length spaces" model of Hofmann in his work on implicit complexity.
Neel Krishnaswami
CC BY-SA 3.0
2012-02-29T13:37:48.827Z
Actually, I wouldn't describe object-based semantics as modeling "linear state".  It is rather "sequential state" and "linear objects", the latte being imposed by SCI.  The games models of Idealized Algol, which are also "object-based" in the same sense, don't have linear anything.
Uday Reddy
CC BY-SA 3.0
2012-02-29T13:38:42.677Z
Can you some references for where such correctness proofs might be found?  (Sorry, turning the question back at you!)
Uday Reddy
CC BY-SA 3.0
2012-02-29T13:55:01.223Z
The simplest soundness proof for a linear language with state I know is Ahmed, Fluet and Morisett's "L3: A Linear Language with Locations". (http://ttic.uchicago.edu/~amal/papers/linloc-fi07.pdf) In the paper, they give a simple logical relation, but mention that a  syntactic progress-and-preservation proof also goes through.
Neel Krishnaswami
CC BY-SA 3.0
2012-03-01T00:37:38.543Z
Here is another piece of work that just came to my attention.  Try citeseer for Stephen Cooper, "On Linear Types and Imperative Update" [link](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.33.6331&rep=rep1&type=pdf).  I should have known about this, but didn't.
Uday Reddy
CC BY-SA 3.0
2012-02-28T21:13:48.597Z
2012-02-28T21:13:48.597Z
Uday Reddy
<p>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). </p>

<p>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 <em>commutative</em> 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.</p>

<p>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?</p>

CC BY-SA 2.5
2010-11-08T22:20:44.153Z
This is the kind of question I would be expecting you to be answering Neel, not asking. ;-)
Marc Hamann
CC BY-SA 2.5
2010-11-11T10:11:27.977Z
if you can attract researchers to cstheory.stackoverflow.com who are capable of answering this question, then the world will be a better place for it.
Dave Clarke
<pl.programming-languages><ct.category-theory><imperative-programming><denotational-semantics><linear-logic>
What is the folk model of linear logic?
Neel Krishnaswami
# What is the folk model of linear logic?

(Asked by: username_0 on 2010-11-08)

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?

**Tags:** pl.programming-languages, ct.category-theory, imperative-programming, denotational-semantics, linear-logic

> **Comments:**
> **username_1**: This is the kind of question I would be expecting you to be answering Neel, not asking. ;-)  
> **username_2**: if you can attract researchers to cstheory.stackoverflow.com who are capable of answering this question, then the world will be a better place for it.  

---

## 2 answers

### Answer by username_2 on 2010-11-11. Score: 9

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](http://www.pps.jussieu.fr/~mellies/papers/ag3-ctcs.pdf). [An algebraic account of references in game semantics](http://www.pps.jussieu.fr/~mellies/papers/mfps2009-references.pdf) 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](http://www.cogs.susx.ac.uk/users/jiml) (such as [A Game Semantics of Names and Pointers](http://www.cogs.susx.ac.uk/users/jiml/pointers3.pdf)) and [Guy McCusker](http://www.cs.bath.ac.uk/~gam23/papers.html) may also contribute to your quest. The recent interesting thesis [Game semantics for an object-oriented language](http://homepages.inf.ed.ac.uk/jrl/Eriskay/wolverson-thesis-final.pdf) 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.

> **Comments:**
> **username_2**: Just curious Neel. Was this of any use to you, or did you know about all of this stuff already?  
> **username_0**: I know this stuff (but not well), but game semantics is a lot more sophisticated than what I'm looking for. Most people have an intuition for linear state which is not far from the old-fashioned Strachey view of an imperative computation as an element of a monadic type $T(A) = S \to A \times S$, and I was hoping there was a model of linear state which would resemble that. Basically, I was hoping there was something you could show a first-year grad student without terrifying them. :)  
> **username_2**: Maybe username_3's Global state considered unnecessary: An introduction to object-based semantics, J. Lisp and Symbolic Computation, 9(1996):7-76.  
> **username_0**: I'm reading that now, actually!  

---

### Answer by username_3 on 2012-02-28. Score: 8

(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.

> **Comments:**
> **username_0**: Actually, it's *too easy* to prove the correctness of implementations of linear state -- linearity is such a strong structural constraint that you hardly need any semantics to do these proofs. As a result, I don't know a simple denotational semantics of linear state. The two closest things to what I want are your work on object-based semantics, and the "length spaces" model of Hofmann in his work on implicit complexity.  
> **username_3**: Actually, I wouldn't describe object-based semantics as modeling "linear state".  It is rather "sequential state" and "linear objects", the latte being imposed by SCI.  The games models of Idealized Algol, which are also "object-based" in the same sense, don't have linear anything.  
> **username_3**: Can you some references for where such correctness proofs might be found?  (Sorry, turning the question back at you!)  
> **username_0**: The simplest soundness proof for a linear language with state I know is Ahmed, Fluet and Morisett's "L3: A Linear Language with Locations". (http://ttic.uchicago.edu/~amal/papers/linloc-fi07.pdf) In the paper, they give a simple logical relation, but mention that a  syntactic progress-and-preservation proof also goes through.  
> **username_3**: Here is another piece of work that just came to my attention.  Try citeseer for Stephen Cooper, "On Linear Types and Imperative Update" [link](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.33.6331&rep=rep1&type=pdf).  I should have known about this, but didn't.  

---

