Mapping intuitionistic logic to the modal logic S4
That is the right paper, but there are actually several equivalent embeddings.

The book Basic Proof Theory by Troelstra and Schwichtenberg gives two such embeddings. Here's one. If $P$ is atomic but not $\bot$:

$$P^\circ := P$$
$$\bot^\circ := \bot$$
$$(A \wedge B)^\circ := A^\circ \wedge B^\circ$$
$$(A \vee B)^\circ := \square A^\circ \vee \square B^\circ$$
$$(A \rightarrow B)^\circ := \square A^\circ \rightarrow B^\circ$$
$$(\exists x A)^\circ := \exists x \square A^\circ$$
$$(\forall x A)^\circ := \forall x A^\circ$$

Here's the other:

$$P^\square := \square P$$
$$\bot^\square := \bot$$
$$(A \wedge B)^\square := A^\square \wedge B^\square$$
$$(A \vee B)^\square := A^\square \vee B^\square$$
$$(A \rightarrow B)^\square := \square (A^\square \rightarrow B^\square)$$
$$(\exists x A)^\square := \exists x A^\square$$
$$(\forall x A)^\square := \square \forall x A^\square$$

They are equivalent in the sense that $S4 \vdash \square A^\circ \leftrightarrow A^\square$, and the embeddings are sound and faithful. The proofs are left as an exercise, or you can dig out the book.