Quantified modal logic and possible world semantics: a uniform approach. The main theme of quantified modal logic is the interplay between modalities (alethic, temporal, etc) and quantification. Combining expressions like "it is possible that", "it is necessary that" with "someone", "everyone", "to be equal to" gives rise to a variety of problems which have a longstanding tradition in philosophy and logic. Let us only mention the well known distinction between modalities "de re" and "de dicto" or the Leibnizian principle of substitutivity. We will try to clarify some of the problems by the help of possible worlds semantics. Two versions will be discussed: Kripke's original one and the one we will call Tarski-Kripke semantics. Formal systems will be presented too and uniform strategies to prove completeness theorems provided.