$\def\dash{\unicode{8212}} \def\trov{\triangleright} \def\ttrov{\triangleright_t} \def\xtrov{\triangleright_x} \def\imp{\Rightarrow} \def\celse{\ |\ } \def\prov{\vdash} \def\dns{{\downarrow}} \def\ups{{\uparrow}} \def\preq{\dashv\vdash} \def\sh{\#} \def\lol{\multimap} \def\lto{\rightarrowtail} \def\rto{\twoheadrightarrow} \def\tensor{\otimes} \def\wat#1{\mathrel{@_{#1}}} \def\ast#1{\mathrel{*_{#1}}} \def\bull#1{\mathrel{\bullet_{#1}}} \def\rle{=}$
Translation
 $P / N$ $P\ast t q / N\ast t f$ $P \lto N$ $\exists \alpha. (P \ast t \alpha) \land \exists \phi . (N \ast t \phi) \land (\alpha \lto \phi \rle f)$ $P \rto N$ $\exists \alpha. (P \ast t \alpha) \land \exists \phi . (N \ast t \phi) \land (\alpha \rto \phi \rle f)$ $P_1 \tensor P_2$ $\exists \alpha_1. (P_1 \ast t \alpha_1) \land \exists \alpha_2 . (P_2 \ast t \alpha_2) \land (\alpha_1 * \alpha_2 \rle q)$ $1$ $1 \rle q$ $N_1 \land N_2$ $N_1 \ast t f \lor N_2 \ast t f$ $P_1 \lor P_2$ $P_1 \ast t q \lor P_2 \ast t q$ $\top$ $\bot$ $0$ $\bot$ $a^-$ $\star_n(a^-, f, t)$ $a^+$ $\star_p(a^+,q, t)$ $\ups P$ $\dns (P \bull t f)$ $\dns N$ $\dns (N \bull t q)$ $\Diamond P$ $f \sqsubseteq t \land \dns \forall x \ge t . P \bull x f$ $\square N$ $q \sqsubseteq t \land \dns \forall x \ge t . N \bull x q$
We translate positive propositions $P$ at resource descriptors' $q$, and negatives $N$ at frame descriptors' $f$. Both translations are also parametrized by a kripke world $t$. These are characterized by:
 Frames $f$ $::=$ $q \lto f \celse q \rto f \celse \phi$ Resources $q$ $::=$ $q \tensor q \celse 1 \celse \alpha$ Kripke Worlds $t$ $::=$ $x$
This definition uses the following abbreviations: $$P \bull t f = \forall \alpha. P \ast t \alpha \imp \alpha \ttrov f$$ $$N \bull t q = \forall \phi. N \ast t \phi \imp q \ttrov \phi$$ A resource is really just a collection of resource variables, which describes the shape of a context, also known as a sequent minus its conclusion. A frame is just a frame variable, with some resource variables glommed onto it, which describes the shape of a sequent minus a hypothesis. We bake in some equalities on worlds and frames to capture the context equivalences of linear logic.

The atomic propositions I'm positing to exist in the destination language are:
• $t_1 \ge t_2$ is a positive atom on two Kripke worlds,
• $f \sqsubseteq t$ is a positive atom on a frame and a world.
• $q \sqsubseteq t$ is a positive atom on a resource and a world.
• $q \ttrov f$ is a negative atom taking a resource, a world, and a frame.
• $\star_n(a^-, f, t)$ is a positive atom taking a negative source-language atom, a frame, and a world.
• $\star_p(a^+, q, t)$ is a positive atom taking a positive source-language atom, a resource, and a world.
Equality on atoms $q \ttrov f$ must at least have the adjunctions $$(q_1 \ttrov q_2 \rto f) = (q_1 \tensor q_2 \ttrov f) = (q_2 \ttrov q_1 \lto f)$$ but we can impose additional axioms to get ordered ($q_1 \tensor (q_2 \tensor q_3) = (q_1 \tensor q_2) \tensor q_3$) or linear ($q_1 \tensor q_2 = q_2 \tensor q_1$) or intuitionistic ($q = 1$) logic.

We also always want the compatibility axioms $$\frac {q \sqsubseteq t \qquad f \sqsubseteq t } {q \lto f \sqsubseteq t} \qquad \frac {q \sqsubseteq t \qquad f \sqsubseteq t } {q \rto f \sqsubseteq t} \qquad \frac {q_1 \sqsubseteq t \qquad q_2 \sqsubseteq t } {q_1 \tensor q_2 \sqsubseteq t} \qquad \frac {} {1 \sqsubseteq t}$$

If you want the modal logic K, don't add any more axioms for $\sqsubseteq$ or $\ge$.

If you want the modal logic T, add reflexivity for $\ge$.

If you want the modal logic K4, add transitivity for $\ge$ and "transitivity" for $\sqsubseteq$: $$\frac {f \sqsubseteq t \qquad t \le t'} {f \sqsubseteq t'} \qquad \frac {q \sqsubseteq t \qquad t \le t'} {q \sqsubseteq t'}$$

If you want the modal logic S4, take the union of the axioms in T and K4.