Located types

Syntax

Extend the syntax of types with:
 
T ::= ...
| at a T (Type Located)
 

Dynamic semantics

Replace the ( Extrusion) rule with:
 
l[new x : resource T; t] new x : at l resource T; l[t] ( Local extrusion)
l[new x : at m resource T; t] new x : at m resource T; l[t] ( Remote extrusion)
 

Static semantics

Add the type judgement:
 
a : location
T : type
(Type Located)
at a T : type
 
Replace the (Net Resource) rule by:
 
at a resource T : type
, x : at a resource T N : network
(Net Resource) [x not in ]
new x : at a resource T; N : network
 
Add the type rule for declarations:
 
T : at a resouce T : type
(Net Remote resource) [x not in ]
new x : at a resource T; : (x : resource T)
 
Replace the (Serializable Resource) rule by:
 
a : location
T : type
(Serializable Located)
at a T : serializable type
 
 Add the subtyping rules:
 
a : here
(Sub Located)
at a T <: T
 

Subject reduction

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