$ \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$