Abstract
Previous type systems for mobility calculi (the original Mobile Ambients, its variants and descendants, e.g., Boxed Ambients and Safe Ambients, and other related systems)offer little support for generic mobile agents. Previous systems either do not handle communication at all or globally assign fixed communication types to ambient names that do not change as an ambient moves around or interacts with other ambients. This makes it hard to type examples such as a messenger ambient that uses communication primitives to collect a message of non-predetermined type and deliver it to a non-predetermined destination.
In contrast, we present our new type system PolyA. Instead of assigning communication types to ambient names, PolyA assigns a type to each process P that gives upper bounds on (1)the possible ambient nesting shapes of any process P’ to which P can evolve, (2)the values that may be communicated at each location, and (3)the capabilities that can be used at each location.Because PolyA can type generic mobile agents, we believe PolyA is the first type system for a mobility calculus that provides type polymorphism comparable in power to polymorphic type systems for the λ-calculas PolyA is easily extended to ambient calculus variants.A restriction of PolyA has principal typings.
Partially supported by EC FP5 grant IST-2001-33477, EPSRC grant GR//R41545/01, NSF grants 9806745 (EIA), 9988529 ((CCR), and 0113193 ((ITR), and Sun Microsystems equipment grant EDUD--7826-990410-US.
Much of the work was done while Amtoft was at Heriot-Watt University paid by EC FP5 grant IST-2001 - 33477.
Chapter PDF
References
T. Amtoft, A. J. Kfoury, S. M. Pericas-Geertsen. What are polymorphically-typed ambients? In D. Sands, ed., ESOP 2001, Genova, vol. 2028 of LNCS. Springer-Verlag, 2001. An extended version appears as Technical Report BUCS-TR-2000-021, Comp.Sci. Department, Boston University, 2000.
T. Amtoft, A. J. Kfoury, S. M. Pericas-Geertsen. Orderly communication in the ambient calculus. Computer Languages, 28, 2002.
T. Amtoft, H. Makholm, J. B. Wells. PolyA: True type polymorphism for Mobile Ambients. Technical Report HW-MACS-TR-0015, Heriot-Watt Univ., School of Math. & Comput. Sci., 2004.
M. Bugliesi, G. Castagna, S. Crafa. Boxed ambients. In 4th International Conference on Theoretical Aspects of Computer Science(TACS’01) vol. 2215 of LNCS. Springer-Verlag, 2001.
L. Cardelli, G. Ghelli, A. D. Gordon. Mobility types for mobile ambients. In J. Wieder-mann et al., eds., ICALP’99, vol. 1644 of LNCS. Springer-Verlag, 1999. Extended version appears as Microsoft Research Technical Report MSR-TR-99-32, 1999.
L. Cardelli, A. D. Gordon. Mobile ambients. In M. Nivat, ed., FoSSaCS’98, vol. 1378 of LNCS. Springer-Verlag, 1998.
L. Cardelli, A. D. Gordon. Types for mobile ambients. In POPL’99, San Antonio, Texas. ACM Press, 1999.
L. Cardelli, P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4), 1985.
M. Coppo, M. Dezani-Ciancaglini. A fully abstract model for higher-order mobile ambients. In VMCAI 2002, vol. 2294 of LNCS, 2002.
M. Coppo, M. Dezani-Ciancaglini, E. Giovannetti, I. Salvo. M3: Mobility types for mobile processes in mobile ambients. In CATS 2003, vol. 78 of ENTCS, 2003.
F. Levi, S. Maffeis. An abstract interpretation framework for analysing mobile ambients. In SAS’01, vol. 2126 of LNCS. Springer-Verlag, 2001.
F. Levi, D. Sangiorgi. Controlling interference in ambients. In POPL’00, Boston, Massachusetts. ACM Press, 2000.
C. Lhoussaine, V. Sassone. A dependently typed ambient calculus. In Programming Languages & Systems, 13th European Symp. Programming, vol. 2986 of LNCS. Springer-Verlag, 2004.
H. Makholm, J. B. Wells. Type inference for PolyA. Technical Report HW-MACS-TR-0013, Heriot-Watt Univ., School of Math. & Comput. Sci., 2004.
R. Milner. Communicating and Mobile Systems: The π-Calculas Cambridge Press, 1999.
F. Nielson, H. R. Nielson, M. Sagiv. A Kleene analysis of mobile ambients. In Programming Languages & Systems, 9th European Symp. Programming, vol. 1782 of LNCS. Springer-Verlag, 2000.
H. R. Nielson, F. Nielson. Shape analysis for mobile ambients. Nordic Journal of Computing, 8, 2001. A preliminary version appeared at POPL’00.
B. C. Pierce, D. Sangiorgi. Behavioralequivalence in the polymorphic pi-calculus. Journal of the ACM, 47(3), 2000.
D. Teller, P. Zimmer, D. Hirschkoff. Using ambients to control resources. In CONCUR’02, vol. 2421 of LNCS. Springer-Verlag, 2002.
D. N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh, 1995. Report no ECS-LFCS-96-345.
J. B. Wells. The essence of principal typings. In Proc. 29th Int’l Coll. Automata, Languages, and Programming, vol. 2380 of LNCS. Springer-Verlag, 2002.
P. Zimmer. Subtyping and typing algorithms for mobile ambients. In FOSSACS 2000, Berlin, vol. 1784 of LNCS. Springer-Verlag, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science + Business Media, Inc.
About this paper
Cite this paper
Amtoft, T., Makholm, H., Wells, J.B. (2004). Polya:True Type Polymorphism for Mobile Ambients. In: Levy, JJ., Mayr, E.W., Mitchell, J.C. (eds) Exploring New Frontiers of Theoretical Informatics. IFIP International Federation for Information Processing, vol 155. Springer, Boston, MA. https://doi.org/10.1007/1-4020-8141-3_45
Download citation
DOI: https://doi.org/10.1007/1-4020-8141-3_45
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4020-8140-8
Online ISBN: 978-1-4020-8141-5
eBook Packages: Springer Book Archive