Mario Coppo, Mariangiola Dezani-Ciancaglini, Elio Giovannetti, and Rosario Pugliese

Dynamic and local typing for mobile ambients

In IFIP TC1 3rd Int'l Conf. Theoret. Comput. Sci. (TCS '04), pages 583-596 Kluwer Academic Publishers, 2004


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.


[ bib | .pdf ]

Back


This file has been generated by bibtex2html 1.43