We present a polynomial translation of the propositional fragment of the modal logic S4 into the propositional fragment of intuitionistic logic. The translation is performed in three main steps. Properties of intermediate translations are established by purely proof-theoretical means, i.e., by proof transformations between different cut-free sequent calculi. Consequently, this approach yields effective translation procedures.