$ \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.
Define the functions $N^w$ and $P^w$ by
$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_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$