$\def\dash{\unicode{8212}} \def\trov{\triangleright} \def\imp{\Rightarrow} \def\celse{\ |\ } \def\prov{\vdash} \def\dns{{\downarrow}} \def\ddns{{\Downarrow}} \def\ups{{\uparrow}} \def\preq{\dashv\vdash} \def\sh{\#} \def\lol{\multimap} \def\tensor{\otimes} \def\wat#1{\mathrel{@_{#1}}} \def\bull#1{\mathrel{\bullet_{#1}}} \def\hole{\unicode{9728}} \def\cn{{:}} \def\here{\dns} \def\dia{{\large\unicode{9671}}}$
Language A
 Negative $N$ $::=$ $P \lol N \celse N \land N \celse \top \celse \dia P \celse a^- \celse \ups P$ Positive $P$ $::=$ $P \tensor P \celse P \lor P \celse 1 \celse 0 \celse \square N \celse a^+ \celse \dns N$
Translation from A to B
We postulate three sorts of first-order terms, frames ($\phi, f, \ldots$) resources ($\alpha, p, \ldots$) and Kripke worlds ($s, t, \ldots$). We overload the symbols $\lol$ and $\tensor$ as example frame and resource constructors.

The expressions $p\trov f$ and $\star(f)$ are negative atoms. Every Language-A atom (regardless of polarity) is mapped to a Language-B positive atom. The expression $s \ge t$ is a positive atom. The expression $\forall s \ge t . N$ abbreviates $\forall s . (s \ge t) \imp N$. $$P^\bullet_t(\phi) = \forall\alpha \cn P^t . (\alpha\trov \phi)$$ $$N^\bullet_t(\alpha) = \forall\phi \cn N^t . (\alpha\trov \phi)$$
 $N$ $N^t$ $P \lol N$ $\exists \alpha \cn P^t . \exists \phi \cn N^t . [\alpha \lol \phi]$ $N_1 \land N_2$ $N_1^t \lor N_2^t$ $\top$ $0$ $\dia P$ $\eta \phi . \star(\phi) \tensor \dns \forall s \ge t . P^\bullet_s(\phi)$ $a^-$ $\eta\phi . a^+(\phi, t)$ $\ups P$ $\eta \phi . \dns P^\bullet_t(\phi)$
 $P$ $P^t$ $P_1 \tensor P_2$ $\exists \alpha_1 \cn P_1^ t. \exists \alpha_2 \cn P_2^ t . [\alpha_1 \tensor \alpha_2]$ $P_1 \lor P_2$ $P_1 ^t \lor P_2 ^ t$ $1$ $[\epsilon]$ $0$ $0$ $\square N$ $\eta \alpha . \dns \forall s \ge t . N^\bullet_s(\alpha)$ $a^+$ $\eta\alpha . a^+(\alpha, t)$ $\dns N$ $\eta \alpha .\dns N^\bullet_t(\alpha)$

Language B
 Prenegative $M$ $::=$ $\dns N \celse a^+(t)\celse M \tensor M$ Negative $N$ $::=$ $\forall x\cn P.N \celse M\imp N \celse N \land N \celse \top \celse a^-(t)$ Positive $P$ $::=$ $\exists x \cn P.P \celse P \lor P \celse 0 \celse [t]\celse \eta x . M$ Contexts $\Gamma$ $::=$ $\cdot \celse \Gamma, M \celse \Gamma, x:P$ Conclusions $K$ $::=$ $t:P \celse N \celse M$
Sequents are either $\Gamma\prov K$. Contex class="right"ts are dependent and therefore ordered. Context variables can appear in the propositions attached to variable bindings to their right, although $x$ may not occur in the $P$ of $x:P$ itself. The metavariable $J$ stands for an arbitrary $\Gamma' \prov K$. When we say $\Gamma \prov J$, we mean $\Gamma, \Gamma' \prov K$. $${\Gamma\prov N \over \Gamma\prov \dns N} \qquad {\Gamma, \dns N \prov J \over \Gamma, N \prov J}$$ $${ \Gamma\prov M_1 \qquad \Gamma\prov M_2\over \Gamma \prov M_1\tensor M_2} \qquad {\Gamma, M_1, M_2 \prov J \over M_1\tensor M_2\prov J}$$ $${\over\Gamma, a^+(t), \Gamma' \prov a^+(t)} \qquad {\over\Gamma, a^-(t), \Gamma' \prov a^-(t)}$$ $${\Gamma, x:P \prov N \over\Gamma \prov \forall x\cn P . N} \qquad {\Gamma\prov t : P \qquad \Gamma, [t/x] N\prov J \over\Gamma, \forall x \cn P . N \prov J}$$ $${\Gamma, M \prov N \over\Gamma \prov M\imp N} \qquad {\Gamma\prov M \qquad \Gamma, N\prov J \over\Gamma, M \imp N \prov J}$$ $${\Gamma, N_i\prov J \over\Gamma,N_1 \land N_2\prov J}\qquad {\Gamma\prov N_1\qquad\Gamma\prov N_2 \over \Gamma \prov N_1 \land N_2 }$$ $${\over \Gamma \prov \top} \qquad{\over \Gamma,0,\Gamma' \prov J} \qquad{\over \Gamma \prov t : 1} \qquad{\over \Gamma \prov t : [t]}$$ $${\Gamma\prov[t/x]J \over\Gamma, x:[t] \prov J}\qquad {\Gamma\prov t : P\qquad \Gamma \prov s : [t/x]P' \over\Gamma \prov s : \exists x\cn P . P'} \qquad {\Gamma, x :P, y : P' \prov J \over\Gamma, y : \exists x \cn P . P' \prov J}$$ $${\Gamma \prov t: P_i\over\Gamma\prov t:P_1 \lor P_2}\qquad {\Gamma, x:P_1\prov J\qquad\Gamma, x:P_2\prov J \over \Gamma, x:P_1 \lor P_2 \prov J}$$ $${ \Gamma\prov [t/x]M \over\Gamma \prov t : \eta x . M }\qquad {\Gamma, y, [y/x]M \prov J \over\Gamma, y : \eta x . M\prov J}$$
Translation from B to C
Translate sequents like this: For all $N$ we have $$\Gamma\prov t : P \qquad\Longleftrightarrow\qquad \forall \Gamma . ((\forall x\cn P^* .N) \imp [t/x]N)$$ And furthermore $$\Gamma\prov N \qquad\Longleftrightarrow\qquad \forall \Gamma . N^*$$ $$\Gamma\prov M \qquad\Longleftrightarrow\qquad \forall \Gamma . M^*$$ Quantify over contexts like this: $$\forall(\Gamma, x :P).N = \forall\Gamma.\forall x\cn P^* . N$$ $$\forall(\Gamma, M).N = \forall\Gamma.M^*\imp N$$ $$\forall(\cdot).N = N$$ What $X^*$ means is a recursive elimination of every $\forall x \cn P.N$ according to this function:
 $P$ $\forall x \cn P . N$ $\exists y \cn P_1 . P_2$ $\forall y \cn P_1 . \forall x \cn P_2.N$ $P_1 \lor P_2$ $\forall x \cn P_1 . N \land \forall x \cn P_2 . N$ $0$ $\top$ $1$ $\forall x . N$ $[t]$ $[t/x]N$ $\eta x \cn P . M$ $\forall x \cn P. (M\imp N)$
Language C
 Prenegative $M$ $::=$ $\dns N \celse a^+(t)$ Negative $N$ $::=$ $\forall x .N \celse M\imp N \celse a^-(t) \celse N \land N \celse \top$ Contexts $\Gamma$ $::=$ $\cdot \celse \Gamma, M$