It is well known that Intuitionistic Logic can be faithfully embedded into (Intuitionistic) Linear Logic. The purpose of this paper is to study the embedding from a semantical viewpoint, by investigating the relationship between various models for Intuitionistic Logic and for Intuitionistic Linear Logic. We will follow this pattern: given a structure that is a model for Intuitionistic Linear Logic we explain how to reconstruct inside it a structure that is a model for Intuitionistic Logic. In the first section this procedure is worked out for the algebraic semantics of quantales with modality. Here it is proved in detail that every quantale with modality gives rise to a frame included in it; furthermore, the isomorphism between the complete lattice of modalities on a quantale and the complete lattice of subframes of a quantale is established. Finally, the largest subframe included in a quantale is described. By a result due to G. Sambin, frames and quantales are representable by means of formal topologies and pretopologies, respectively. In the appendix, an extension of these representation theorems to quantales with modality is used to show that any quantale with modality is isomorphic to the class of saturated subsets of a suitable pretopology endowed with an operator, called the stable interior operator [\textit{G. Sambin}, Logic Colloq. '88, Proc. Colloq., Padova / Italy 1988, Stud. Logic Found. Math. 127, 261-285 (1989; Zbl 0677.03006)]. As an application, we show how, given a formal pretopology with a stable interior operator representing a quantale, we can obtain a formal topology representing the subframe determined by the modality. All these semantical considerations lead us to consider, in the second section, `natural' requirements on translations from Intuitionistic Logic into Intuitionistic Linear Logic. More explicitly, we define a faithful translation corresponding to the insertion of a subframe into its matching quantale with modality, and such that translated formulas are equivalent to their exclamation. Furthermore, we define a faithful translation which is also a translation of schemes, that is which commutes with substitution. In the final section we deal with categorical semantics, which has been extensively studied in the Linear Logic literature. We study sufficient (and in a way necessary) conditions such that the co-Kleisli construction, applied to a category that is a model for Linear Logic, gives rise to a categorical model for Intuitionistic Logic. In particular, we propose an answer to a question, raised by \textit{R. A. G. Seely} [Contemp. Math. 92, 371-382 (1989; Zbl 0674.03007)], concerning the existence of coproducts in the co-Kleisli category. Finally, we show that the algebraic construction developed in the first part is just a particular case of this categorical one, namely its reduction to partial orders.