Pfenning and Davies present a translation on p.22 of the following reference:
The translation is from propositional lax logic ($PLL$) into a constructive modal logic which adjoins to the intuitionistic propositional calculus two modal operators $\Diamond, \Box$ obeying the characteristic features of S4 modalities (see 4.3 and 5.3 in their article). Alechina, et al http://www.cs.nott.ac.uk/~psznza/papers/Alechina++:01a.pdf , discuss a modal logic $CS4$ with the same modal axioms, as Derek Elkins has pointed out below.
Here (see p.22 of Pfenning and Davies' article) is the translation from $PLL$ to constructive S4 ($\bigcirc$ is the modal operator of $PLL$ and “·” indicates an empty collection of hypotheses):
$$(A ⇒ B)^+ = \Box A^+ ⊃ B^+$$ $$(\bigcirc A)^+ = \Diamond \Box A^+$$ $$P^+ = P \hspace{0.5cm} \text{for atomic} \thinspace P$$ $$(·)^+ = ·$$ $$(Γ, A \hspace{0.3cm} \text{true})^+ = Γ^+, A^+ \hspace{0.3cm} valid$$
$CS4$ (and therefore Pfenning and Davies' logic) lacks the distributive axiom $\Diamond (A \lor B) \rightarrow \Diamond A \lor \Diamond B$ and does not validate $¬\Diamond ⊥$, i.e., in these logics ($\Diamond ⊥$) and (⊥) are not equiprovable (which is the nullary form of the distribution).
Unfortunately, the proof systems for Intuitionistic $S4$ are quite obscure (see for example the tableaux discussed in A complicated, curious tableaux proof rule for Intuitionistic S4 )
I would like to know:
(1) whether Pfenning and Davies translation from $PLL$ to their logic can be used as a translation from $PLL$ to other variants of intutionistic $S4$, which perhaps do not lack the distributive property $\Diamond (A \lor B) \rightarrow \Diamond A \lor \Diamond B$ (such as the variant discussed in the question A complicated, curious tableaux proof rule for Intuitionistic S4)
(2) whether the axiom of $PLL$ $(A \rightarrow \bigcirc B) \equiv (\bigcirc A \rightarrow \bigcirc B)$ (which bears a relation to the operations of a strong monad and those of the Kleisli category) is valid when it is translated into other versions of Intuitionistic $S4$, perhaps via the same translation from $PLL$ to $CS4$ that Pfenning and Davies propose (Pfenning and Davies' translation of this axiom is $(\Box A \rightarrow \Diamond \Box B) \equiv (\Box \Diamond \Box A \rightarrow \Diamond \Box B)$). (Then I would like to see whether certain characteristic theorems of $PLL$ are provable in these other variants of intuitionistic $S4$.)
(3) whether the translation of Pfenning and Davies is related to the translation of $PLL$ into classical bimodal $S4, S4$, that Fairtlough and Mendler define in their original paper on $PLL$, on page 20 of the following:
$\underline{Bonus}$: If you know of a proof system for an intuitionistic modal $S4$ that is easy to work with (preferably a tableau system or sequent calculus and perhaps even a natural deduction system), I would be very interested.