Abstract
The Ambient Calculus was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code [6]. We consider an Ambient Calculus where ambients transport and exchange programs rather that just inert data. We propose different senses in which such a calculus can be said to be polymorphically typed, and design accordingly a polymorphic type system for it. Our type system assigns types to embedded programs and what we call behaviors to processes; a denotational semantics of behaviors is then proposed, here called trace semantics, underlying much of the remaining analysis.We state and prove a Subject Reduction property for our polymorphically-typed calculus. Based on techniques borrowed from finite automata theory, type-checking of fully type-annotated processes is shown to be decidable. Our polymorphically-typed calculus is a conservative extension of the typed Ambient Calculus originally proposed by Cardelli and Gordon [7].
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Torben Amtoft, Assaf J. Kfoury, and Santiago Pericas-Geersten. What are polymorphically-typed ambients? Technical Report BUCS-TR-2000-021, Comp. Sci. Dept., Boston Univ., December 2000.
Torben Amtoft, Flemming Nielson, and Hanne Riis Nielson. Type and Effect Systems: Behaviours for Concurrency. Imperial College Press, 1999.
Michele Bugliesi, Giuseppe Castagna, and Silvia Crafa. Typed mobile objects. In CONCUR 2000, volume 1877 of LNCS, pages 504–520, 2000.
Luca Cardelli. Abstractions for mobile computation. In Jan Vitek and Christian Jensen, editors, Secure Internet Programming: Security Issues for Mobile and Distributed Objects, volume 1603 of LNCS, pages 51–94. Springer-Verlag, 1999.
Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon. Mobility types for mobile ambients. In Jiri Wiedermann, Peter van Emde Boas, and Mogens Nielsen, editors, ICALP’99, volume 1644 of LNCS, pages 230–239. Springer-Verlag, July 1999.
Luca Cardelli and Andrew D. Gordon. Mobile ambients. In Maurice Nivat, editor, FoSSaCS’98, volume 1378 of LNCS, pages 140–155. Springer-Verlag, 1998.
Luca Cardelli and Andrew D. Gordon. Types for mobile ambients. In POPL’99, San Antonio, Texas, pages 79–92. ACM Press, January 1999.
Cedric Fournet, Georges Gonthier, Jean-Jacques Levy, Luc Maranget, and Didier Remy. A calculus of mobile agents. In CONCUR 1996, volume 1119 of LNCS, pages 406–421. Springer-Verlag, 1996.
Simon Gay and Malcolm Hole. Types and subtypes for client-server interactions. In Proc. European Symp. on Programming, volume 1576 of LNCS, pages 74–90. Springer-Verlag, 1999.
Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP’98, volume 1381 of LNCS, pages 122–138. Springer-Verlag, 1998.
Francesca Levi and Davide Sangiorgi. Controlling interference in ambients. In POPL’00, Boston, Massachusetts, pages 352–364. ACM Press, January 2000.
Eugenio Moggi. Arity polymorphism and dependent types. In Subtyping & Dependent Types in Programming, Ponte de Lima, Portugal, 2000. Proceedings online at http://www-sop.inria.fr/oasis/DTP00/Proceedings/proceedings.html.
Hanne Riis Nielson and Flemming Nielson. Shape analysis for mobile ambients. In POPL’00, Boston, Massachusetts, pages 142–154. ACM Press, 2000.
Benjamin C. Pierce and Davide Sangiorgi. Types and subtypes for mobile processes. Mathematical Structures in Computer Science, 6(5):409–454, 1996. A revised and extended version of a paper appearing at LICS’93.
Benjamin C. Pierce and David N. Turner. Pict: A programming language based on the pi-calculus. Technical report, IU, 1997.
James Riely and Matthew Hennessy. Trust and partial typing in open systems of mobile agents. In POPL’99, San Antonio, Texas, pages 93–104. ACM Press, 1999.
Peter Sewell and Jan Vitek. Secure composition of insecure components. In 12th IEEE Computer Security Foundations Workshop (CSFW-12), Mordano, Italy, June 1999.
Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interaction-based language and its typing system. In PARLE’94, volume 817 of LNCS, pages 398–413. Springer-Verlag, 1994.
David N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh, 1995. Report no ECS-LFCS-96-345.
Jan Vitek and Giuseppe Castagna. Seal: A framework for secure mobile computations. In Internet Programming Languages, volume 1686 of LNCS. Springer-Verlag, 1999.
Nobuko Yoshida and Matthew Hennessy. Subtyping and locality in distributed higher order mobile processes. In CONCUR 1999, volume 1664 of LNCS, pages 557–573. Springer-Verlag, 1999.
Nobuko Yoshida and Matthew Hennessy. Assigning types to processes. In LICS 2000, pages 334–345, 2000.
Pascal Zimmer. Subtyping and typing algorithms for mobile ambients. In FOS-SACS 2000, Berlin, volume 1784 of LNCS, pages 375–390. Springer-Verlag, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amtoft, T., Kfoury, A.J., Pericas-Geertsen, S.M. (2001). What Are Polymorphically-Typed Ambients?. In: Sands, D. (eds) Programming Languages and Systems. ESOP 2001. Lecture Notes in Computer Science, vol 2028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45309-1_14
Download citation
DOI: https://doi.org/10.1007/3-540-45309-1_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41862-7
Online ISBN: 978-3-540-45309-3
eBook Packages: Springer Book Archive