Every once in a while this last week I keep going back to this email that Frank had cc'ed me on along with a bunch of other people, about some recent thoughts he had on session types and focusing and stuff. It reminds me that I never really understood session types hardly at all, since Frank and Luís's big paper on the Curry-Howardizing of them was from 2010, after I'd already left pittsburgh for philadelphier pastures. 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