Mapping intuitionistic logic to the modal logic S4

In his famous Semantical Analysis of Intuitionistic Logic,
S. Kripke speaks of the "well-known mappings of intuitionistic logic
into the modal system S4". I'm not sure which mappings Kripke means.
One guess would be K. Gödel's "Eine Interpretation des
Intuitionistischen Aussagenkalküls" (translated into English as "An
Interpretation of the Intuitionistic Propositional Calculus". I don't have
access to either.)

Could somebody please point me towards a text that details these
translations?

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.

StackExchange Computer Science Q#22218, answer score: 9