We consider a simple language of processes and an expressive language of formulas. The former is the non-deterministic choice free fragment of Milner's CCS, while the latter is inspired on the Spatial Logic of Caires and Cardelli and on the Process Logic of Milner. We adopt a "propositions as types" approach, where types are formulas, denotational semantics are established through structural congruence and labelled transitions, and subtyping is interpreted as a kind of logical entailment. A type system is defined as a deductive system and some results are proved about it, namely weak consistency and completeness. Finally, an application of the system is developed, thus expressing its potential.