...

Every input expression is associated with the namespace of the names it is listening on.  Cross-namespace joins are forbidden, so the namespace is unique.  Every output expression is associated with the namespace of the name being sent on.  When sending or listening on a public name, it must be annotated with a namespace.  Every new production annotates each new name with a namespace.  Other productions live in the nearest enclosing input.

...

Mobility

Consider the case where b is in the namespace B, y is in the namespace Y, and the following process is running (necessarily in the namespace B by the previous paragraph):

...

but that ought to run in the namespace Y, so B then deploys transfers y!(Q) to Y and removes it from its own state.

A datafeed gets implemented as followsSimilarly, consider the case where b is in the namespace B, y is in the namespace Y, and the following process is running in B:

    new ret in {
      dataFeed!(ret) |
      for (datafor(a <- b) { for (c <- reta) {
 Q } } |    handleb!(data*y)

The process reduces to

    for (c }
<- y) { Q }

but that ought to run in the namespace Y, so B then transfers for (c <- y) { Q } to Y and removes it from its own state.

In both cases, the validators in Y need to receive enough messages from B that Y can be sure that B won't roll back the transfer.

Joins

Joins between names that are not in the same namespace is a type error.  If a process in the namespace B and a process in the namespace Y wish to race, then they should send messages to a process in the namespace B∨Y. 

...