Title: Reasoning about Resource Management for Message Passing Concurrency

Abstract: 
We define a  \pic variant with a costed semantics where channels are treated as
resources that must explicitly be allocated before they are used and can be
deallocated when no longer required. We use a substructural type system
tracking permission transfer to construct compositional proof techniques for
comparing behaviour and resource usage efficiency of concurrent processes.