We present a type system to guarantee termination of pi-calculus processes that exploits input/output capabilities and subtyping, as originally introduced by Pierce and Sangiorgi, in order to analyse the usage of channels. We show that our system imp
roves over previously existing proposals by accepting more processes as terminating. This increased expressiveness allows us to capture sensible programming idioms. We demonstrate how our system can be extended to handle the encoding of the simply typed lambda-calculus, and discuss questions related to type inference.
We provide a characterisation of strong bisimilarity in a fragment of CCS that contains only prefix, parallel composition, synchronisation and a limited form of replication. The characterisation is not an axiomatisation, but is instead presented as a
rewriting system. We discuss how our method allows us to derive a new congruence result in the $pi$-calculus: congruence holds in the sub-calculus that does not include restriction nor sum, and features a limited form of replication. We have not formalised the latter result in all details.
