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}⊸ A

^{00}⊕ B

^{00}(where X

^{0}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

**inl**s and

**inr**s 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