The aim of our work is the definition of a model-theoretic semantics of normal logic programs with embedded implications. We first propose a quite simple operational semantics for this class of programs whose negation mechanism is the constructive negation. This semantics is used to prove the adequacy of the model-theoretic semantics. Then we define a declarative semantics for this class of programs in terms of Beth models and show that in the model class associated to every program there is a least model that can be seen as the semantics of the program, which may be built upwards as the least fixpoint of a continuous immediate consequence operator. Finally, it is proved that the operational semantics is sound and complete with respect to the least fixpoint semantics.