A proof of the focalization property of linear logic, Olivier Laurent. Looks like it might be a classical version of the focusing proof I just thought of yesterday.
From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic, Miller and Saurin.
Whatever Anders has written about the pattern fragment for LLF, which I can't seem to find right now. Hrm.
