$\def\imp{\Rightarrow} \def\celse{\ |\ } \def\prov{\vdash} \def\dns{{\downarrow}} \def\ups{{\uparrow}} \def\preq{\dashv\vdash} \def\sh{\#} \def\tensor{\land^+}$
Source Language
The source language is a straightforward polarized modal language. Its syntax goes like this:
 Negative $N$ $::=$ $P \imp N \celse N \land N \celse \top \celse \Diamond 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$
Target Language
The target language is just ordinary focused first order logic, nothing surprising. Pick one distinguished negative atomic formula $h(w, \phi, m)$ (pronounced 'here') with three arguments.
• $w$ is the Kripke modal world for the modal logic of $\square$ and $\Diamond$.
• $\phi$ can be seen as a modal world in the sense that intuitionistic logic is a modal logic over classical logic. We shunt conclusions into the context, (arguably a classical-logical sort of trick to pull) so we need $\phi$ to make sure only the 'fresh' ones can be used.
• $m$ is a parameter used to enforce the condition that $\Diamond$ can only be unpacked on the left when the conclusion is $\mathrm{poss}$. There is a distinguished first-order term $\star$ constant which may appear in the third argument of $h$.
Translation
Define the functions $N^w$ and $P^w$ by
 $N$ $N^w$ $P \imp N$ $P^w \imp N^w$ $N_1 \land N_2$ $N_1^w \land N_2^w$ $\top$ $\top$ $\Diamond P$ $\forall \phi . \dns (\forall v \ge w . P^v \to h(v \phi \star)) \to h(w \phi \star)$ $a^-$ $\forall \phi m . a^+(w\phi) \to h(w \phi m)$ $\ups P$ $\forall \phi m . \dns (P^w \to h(w \phi m)) \to h(w \phi m)$
 $P$ $P^w$ $P_1 \tensor P_2$ $P_1^w \tensor P_2^w$ $P_1 \lor P_2$ $P_1^w \lor P_2^w$ $1$ $1$ $0$ $0$ $\square N$ $\dns \forall v \ge w . N^v$ $a^+$ $a^+(w)$ $\dns N$ $\dns N^w$