This report develops the theory of a modal process logic first introduced by Kim Larsen and Bent Thomsen. The logic can be seen as an extension of CCS and has an operational semantics upon which a preorder on formulae in the logic is defined. A denotational description originally put forward by Kim Larsen and Bent Thomsen is examined, and it is shown to what extent the refinement ordering explains the ordering introduced by this kind of semantic description. In particular it is shown how the modal process logic semantically subsumes the language of partial specifications also introduced by Kim Larsen and Bent Thomsen. The static constructs of CCS are added to the logic, and a new `observational'' preorder is introduced and used on three examples. Finally, sound and complete proof systems are given for the strong refinement ordering and the equality defined by the denotational semantics.