I am looking for papers and articles on modal substructural logics-- not on the semantics of linear logic modalities, but on substructural logics augmented with standard modal operators, e.g. substructural K (something like MALL with box operator, necessitation and K rules).
I know of work adding temporal modalities to linear logic to produce what has been called temporal linear logic (in contrast to LTL = linear-time temporal logic). This is quite interesting: a formula (without a modality) is interpreted as resources being available now. The next time modality $\bigcirc-$ is interpreted as resources being available in the next time step. The box modality $\Box-$ means that the resources can be consumed at any point in the future, determined by the holder of the resources, whereas $\lozenge-$ means that the resources can be consumed at any point in time determined by the system. Notice the duality between the holder of the resource and the system.
Banbara, M., Kang, K.-S., Hirai, T., Tamura, N.: Logic programming in a fragment of intuitionistic temporal linear logic. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, pp. 315–330. Springer, Heidelberg (2001)
Hirai, T.: Propositional temporal linear logic and its application to concurrent systems. EICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences (Special Section on Concurrent Systems Technology) E83- A(11), 2219–2227 (2000)
Hirai, T.: Temporal Linear Logic and Its Application. PhD thesis, The Graduate School of Science and Technology, Kobe University, Japan (September 2000).
Kamide, N.: Temporalizing Linear Logic Bulletin of the Section of Logic Volume 36:3/4 (2007), pp. 173–182
There are a few papers adding all sorts of modalities to linear and affine logic:
Kamide, N.: Linear and affine logics with temporal, spatial and epistemic logics. Theoretical Computer Science 252, 165–207 (2006).
Kamide, N: Combining Soft Linear Logic and Spatio-Temporal Operators. J Logic Computation (2004) 14 (5): 625-650.
The work on temporal linear logic has been applied in agent-oriented programming and coordination, making essential use of the interpretation of the modalities described above:
Kungas, P.: Temporal linear logic for symbolic agent negotiation. In: Zhang, C., W. Guesgen, H., Yeap, W.-K. (eds.) PRICAI 2004. LNCS, vol. 3157, pp. 23–32. Springer, Heidelberg (2004)
Pham, D.Q., Harland, J., Winikoff, M.: Modelling agent’s choices in temporal linear logic. In: Baldoni, M., Son, T.C., van Riemsdijk, M.B., Winikoff, M. (eds.) DALT 2007. LNCS, vol. 4897, pp. 140–157. Springer, Heidelberg (2008)
Clarke, D. Coordination: Reo, Nets and Logic. FMCO proceedings, LNCS, vol. 5382. (2008)
These kind of logics are considered in linguistics: you can have a look at Michael Moortgat's article, Categorial Type Logic.
The !A modality of linear logic is a box operator satisfying the S4 axioms.
It's well-known that the uniqueness of !A is not derivable -- that is, if you have a red bang and a blue bang, both of which separately satisfy the rules for bang, you can't prove that they are equivalent. I don't recall offhand where this result can be found, but it's probably in Girard's 1987 paper on linear logic.
EDIT: I asked Jason Reed, whose thesis was about encodings of linear logic into hybrid logic, and he pointed me at the following paper by Chaudhuri and Despeyroux, "A Logic for Constrained Process Calculi with Applications to Molecular Biology". They extend intuitionistic linear logic with hybrid annotations intended to mirror temporal logic, and they did a very clean job of it -- they prove not just have cut-elimination, but also focalization. So it looks like it should be straightforward to simplify their calculus to get modal K a la Simpson.
Currently, the most systematic proof theory that allows many modal logics to be layered upon many substructural logics is Belnap's display logic, which has received a decent treatment at the hands of Marcus Kracht —see in particular his Power and Weakness of the Modal Display Logic, 1996— and Heinrich Wansing, Displaying Modal Logic, 1998.
Display logic has problems handling noncommutative logic, which was one of the motivations behind a couple of MSc theses I supervised some years back, to apply some ideas about representing modalities in the Calculus of Structures, which is very powerful for representing substructural logics, but ran into problems because of the unusual way cut-elimination is proven in that setting. Robert Hein's work on generating rules for modal logics from families of axioms, summarised in Purity through Unravelling, 2005, covers most of the usual logics (the most important axioms not covered are B, CR, and L), and there is fairly strong circumstantial evidence to believe the cut-elimination conjecture. None of this work actually treats substructural logic, but if a stronger kind of cut-elimination theorem were proven for these modalities, the so-called splitting lemma, this would make the logic very modular and cut-elimination should follow easily for all ways of gluing together the logics.
Substructural logic doesn't really have a uniform notion of semantics, but for modal substructural logic we do have a kind of recipe for turning semantics of the base logic into semantics of matching modal logics, by extending a trace-like semantics with a notion of frame or an algebraic/categorical semantics with a notion of operator. Kracht and Wansing do some work in both of these directions.
I've been skimming Norihiro Kamide, "Kripke Semantics for Modal Substructural Logics", Journal of Logic, Language and Information 11 (4), 2002, which isn't quite what I wanted, but the references cite Marcello D'Agostino and Dov M. Gabbay and Alessandra Russo, "Grafting Modalities onto substructural implication systems", Studia Logica 59, 1996, which seems to be what I am looking for. It is on CiteSeer http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5719