Time: Thursday, March 20, 14.30-15.30
Place: C3-204
We propose a calculus of copyable mobile resources, in which movement of resources to and from slots are the only communication primitives. The calculus generalises the calculus of Mobile Resources (proposed by Godskesen, Hildebrandt and Sassone at CONCUR2002) to allow general, non-linear substitution of the moved resources into the moving process, as found in CHOCS and the lambda-calculus. We propose a simple, novel type system, that allows a distinction between copyable and non-copyable resources. This is done by having two types of slots, namely hard and soft slots. A soft slot is one that contains copyable resources, say software, whereas resources in hard slots, say hardware, cannot be copied. To support reasoning about behaviours of systems in the calculus, we provide a labelled transition semantics and prove correspondence between weak barbed bisimulation congruence and weak labelled transition bisimulation congruences.