Avoiding grave interference in BoCa

The grave interferences in the calculus of bounded capacities(BoCa) can be regarded as programming errors and could be disastrous. In order to avoid the problems and to control the movement of resources, some BoCa primitives are modified. A new calculus, the safe bounded capacities (Safe BoCa) is proposed that modifies two capacities and adds three new capabilities and two new co-capabilities. The reduction semantics is modified accordingly. A type system for the safe BoCa is given to control the mobility of ambients and the number of threads, and to guarantee that the intended capacity bounds are statically preserved throughout computation.