Trying to digest that earlier paper now, I still have two big questions I don't know how to answer well, which are basically
(a) what happens with classical logic instead of intuitionistic?
(b) what happens with a symmetric tensor/lollipop instead of asymmetric?
As for (a), is the answer that standard session type systems connected to classical logic? Or no logic at all? I have no idea. All I know is it appears perfectly easy to start with [Concur10] and simply drop the requirement that the right-hand side of the sequent always has cardinality 1. I can make up some rules for par, I can prove classical linear logic shibboleths like (A ⊕ B)00 ⊸ A00 ⊕ B00 (where X0 means X ⊸ 0) like it's no big deal, and I get what seems to me to be a reasonable-looking process expression --- but maybe it lacks some important session-types-y property that I'm not familiar with.
For (b) I mean instead of rules like
Δ, y : A, x : B ⊢ P :: T ----------------------------⊗L Δ, x : A ⊗ B ⊢ x(y).P :: T Δ2 ⊢ Q :: y : A Δ1 ⊢ P :: x : B ----------------------------⊗R Δ1, Δ2 ⊢ (νy)x⟨y⟩.(P|Q) :: x : A ⊗ B
you could have rules like
Δ, y : A, z : B ⊢ P :: T ----------------------------⊗L Δ, x : A ⊗ B ⊢ x(y,z).P :: T Δ2 ⊢ Q :: y : A Δ1 ⊢ P :: z : B ----------------------------⊗R Δ1, Δ2 ⊢ (νy)(νz)x⟨y,z⟩.(P|Q) :: x : A ⊗ B
Now this requires having a primitive notion of sending (and receiving) a pair of channel names along a channel, but the treatment of additive disjunction and conjunction already required postulating the ability to perform inls and inrs and case operations on channels, so I think that's not objectionable.
what this does though is make x into not really a channel that gets reused at a different type at a later time during the session, but rather something that gets assigned a value once and only once. I think you can go farther and make all the session-type rules like this (observing that the shifts in the focusing treatment in Frank's recent note already have this property) so that it ceases to be a system of (nontrivial) channels at all, but something more like futures --- which I guess is kind of another way of viewing channels that only ever transmit one value, anyhow.
I wonder if this observation has any value, or whether on the other hand I might just recapitulating the history of session type research in reverse, by stripping away everything people actually like about them :P
