Dynamic and Local Typing for Mobile Ambients.
Elio Giovannetti
Abstract
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
an ambient or process has the right to go; dynamic type-checking
controls ``passive'' rights, i.e., which ambients one may be crossed
by and which processes one may receive.