Distributed resource calculus

Syntax

Let l, m, n range over locations (Loc).

Let a, b, c range over names (Var union Loc).

Replace  the syntactic category (Net Thread) by:

 
N ::= ...
| l[t] (Net Located thread)
 
 Extend the syntax of threads:
 
t ::= ...
| at a t (Thread Migration)
 
Extend the syntax of values:
 
v ::= ...
| l (Val Location)
 
Extend the syntax of types:
 
T ::= ...
| location (Type Location)
 

Dynamic semantics

Structural equivalence is as before, but with the addition of locations on threads in the let associativity rule:
 
l[let p = D e; t] l[D let p = e; t] (Let Assoc) [bv D disjoint fv t]
 
Reduction is as before, but with the addition of locations on threads:
 
l[spawn t; u]
 l[t] | l[u] ( Spawn)
l[register x = v] | l[let p = access x; t]
 l[register x = v] | l[t[v/p]] ( Fetch)
l[new x : resource T; t] new x : resource T; l[t] ( Extrusion)
l[let p = v w; t] l[let p = e[v/x,w/q]; t] ( Fun beta) [v = function x q : T {e}]
l[let p = v; t] l[t[v/p]] ( Let beta)
l[stop] 0 ( Garbage)
 
The new rule is:
 
l[at m t]
 m[t] ( Migration)
 

Static semantics

Extend the judgements of types with:
 
(Type Location)
location : type
 
Replace the type rule (Net Thread) by:
 
t : thread
(Net Located thread)
l[t] network
 
Extend the type rules for threads with:
 
a : location
t : thread
(Thread Migration)
at a t : thread
 
Extend the type rules for values with:
 
(Val Location)
l : location
 

Subject reduction

Proposition If  N : network and N * M then  M : network.