Has anyone studied a version of linear logic in which the storage modality $!$ preserves the positive connectives and quantifiers $\otimes,\oplus,\exists$? That is, such that we have $!(A\otimes B) = !A \otimes !B$ and $!(A\oplus B) = !A \oplus !B$ and $!\exists x. A = \exists x.!A$. It seems that there ought to be a reasonable sequent calculus for such a theory, e.g. using a "modal context zone" as in Girard's LU or Pfenning's LV enhanced with left rules that allow introducing $\otimes,\oplus,\exists$ in the modal zone.