Dynamic and Local Typing for Mobile Ambients
Mario Coppo, Mariangiola Dezani-Ciancaglini, Elio Giovannetti, Rosario Pugliese · Kluwer Academic Publishers eBooks · 2006
An ambient calculus with both static and dynamic types is presented, where the latter ones represent mobility and access rights that may be dynamically consumed and acquired in a controlled way. Novel constructs and operations are provided to this end. Type-checking is purely local, except for a global hierarchy that establishes which locations have the authority to grant rights to which: there is no global environment (for closed terms) assigning types to names. Each ambient or process move is subject to a double authorization, one static and the other dynamic: static type-checking controls (communication and) “active” mobility rights, i.e., where a given ambient or process has the right to go; dynamic type-checking controls “passive” rights, i.e., which ambients a given ambient may be crossed by and which processes it may receive.