Compositional Reasoning for Channel-Based Concurrent Resource Management
Adrian Francalanza, Edsko de Vries, Matthew Hennessy · 2012
Abstract: We define a pi-calculus variant with a costed semantics where chan-nels 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 tech-niques for comparing behaviour and resource usage efficiency of concurrent processes.