I finally wrote up "Focusing as Token-Passing", because it seemed to be important to clarify those ideas before moving on to the modal logic stuff I wanted to say, since understanding the innards of pfenning-davies box (resp. diamond, circle) seems to depend on really understanding the downshift (resp. upshift, [and again for circle also] upshift) contained within it.
It is a "theorems for cheap" sort of paper. Given "microfocused" connectives q⊗ and q⊸ (for an an atomic proposition q) whose right and left rules respectively demand the atom be in the context right now you can simulate all of focusing inside linear logic. Then you can prove all the theorems you want (cut-elim and identity for the focusing logic, completeness of focusing) and you can prove them internally by splicing together easy-to-prove propositional equivalence derivations. The real point is that even if the translations are a little involved, the proof is O(n) big in the number of connectives because it is modular, rather than O(n2) big, like other proofs that consider how different connectives interact. It also implements the ordered asynchronous context used in focusing without having any ordered contexts in the host language, by doing a little destination-passing trick.
I think of it as a sequel to "Focalizing Linear Logic in Itself". The main difference is that I don't sweep the asynchronous stuff under the rug here: the entire machinery of focusing can be faithfully simulated with token-passing. Also it's just a little bit less sloppy of a paper all around I think.
Turned out to be 13 pages even while I was trying not to be particularly unterse about it. Still not an unreadable length, I hope. I would super-appreciate comments. Especially if you think you should be able to make sense out of it because of the material (and really, I think this is anyone who knows linear logic and a is at least a little familiar with focusing) but are unable to because of the quality of the writing.