It is arguably desirable to have a theory of meaning that (i) does not identify propositions with sets of worlds, (ii) enables to capture the dynamic character of semantic interpretation and (iii) provides the basis for a semantic program that incorporates and extends the achievements of Montague semantics. A theory of properties and propositions that meets these desiderata is developed and several applications to the semantic analysis of natural languages are explored.