Soundness of labelled deduction. August, 2005.
An attempt at a constructive proof of the soundness of labelled deduction for intuitionistic logic. This is essentially a variation on the usual "prime context" approach establishing completeness of intuitionistic logic with respect to Kripke semantics.
For a more novel approach, see Jason Reed and Frank Pfenning's "Intuitionistic letcc via labelled deduction".
Modal BI and Separation Logic. June, 2005. Describes how to extend the logic of bunched implications with an S4-like box modality, and its relationship to "purity" in separation logic.