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. © 2004 Springer Science + Business Media, Inc.
CITATION STYLE
Coppo, M., Dezani-Ciancaglini, M., Giovannetti, E., & Pugliese, R. (2004). Dynamic and local typing for mobile ambients. In IFIP Advances in Information and Communication Technology (Vol. 155, pp. 577–590). Springer New York LLC. https://doi.org/10.1007/1-4020-8141-3_44
Mendeley helps you to discover research relevant for your work.