What Are Polymorphically-Typed Ambients?

  • Torben Amtoft
  • Assaf J. Kfoury
  • Santiago M. Pericas-Geertsen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)


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].


Denotational Semantic Conservative Extension Type Check Trace Semantic Subject Reduction 
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.


  1. [1]
    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.Google Scholar
  2. [2]
    Torben Amtoft, Flemming Nielson, and Hanne Riis Nielson. Type and Effect Systems: Behaviours for Concurrency. Imperial College Press, 1999.Google Scholar
  3. [3]
    Michele Bugliesi, Giuseppe Castagna, and Silvia Crafa. Typed mobile objects. In CONCUR 2000, volume 1877 of LNCS, pages 504–520, 2000.CrossRefGoogle Scholar
  4. [4]
    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.Google Scholar
  5. [5]
    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.Google Scholar
  6. [6]
    Luca Cardelli and Andrew D. Gordon. Mobile ambients. In Maurice Nivat, editor, FoSSaCS’98, volume 1378 of LNCS, pages 140–155. Springer-Verlag, 1998.Google Scholar
  7. [7]
    Luca Cardelli and Andrew D. Gordon. Types for mobile ambients. In POPL’99, San Antonio, Texas, pages 79–92. ACM Press, January 1999.Google Scholar
  8. [8]
    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.Google Scholar
  9. [9]
    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.Google Scholar
  10. [10]
    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.Google Scholar
  11. [11]
    Francesca Levi and Davide Sangiorgi. Controlling interference in ambients. In POPL’00, Boston, Massachusetts, pages 352–364. ACM Press, January 2000.Google Scholar
  12. [12]
    Eugenio Moggi. Arity polymorphism and dependent types. In Subtyping & Dependent Types in Programming, Ponte de Lima, Portugal, 2000. Proceedings online at
  13. [13]
    Hanne Riis Nielson and Flemming Nielson. Shape analysis for mobile ambients. In POPL’00, Boston, Massachusetts, pages 142–154. ACM Press, 2000.Google Scholar
  14. [14]
    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.zbMATHMathSciNetGoogle Scholar
  15. [15]
    Benjamin C. Pierce and David N. Turner. Pict: A programming language based on the pi-calculus. Technical report, IU, 1997.Google Scholar
  16. [16]
    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.Google Scholar
  17. [17]
    Peter Sewell and Jan Vitek. Secure composition of insecure components. In 12th IEEE Computer Security Foundations Workshop (CSFW-12), Mordano, Italy, June 1999.Google Scholar
  18. [18]
    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.Google Scholar
  19. [19]
    David N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh, 1995. Report no ECS-LFCS-96-345.Google Scholar
  20. [20]
    Jan Vitek and Giuseppe Castagna. Seal: A framework for secure mobile computations. In Internet Programming Languages, volume 1686 of LNCS. Springer-Verlag, 1999.Google Scholar
  21. [21]
    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.Google Scholar
  22. [22]
    Nobuko Yoshida and Matthew Hennessy. Assigning types to processes. In LICS 2000, pages 334–345, 2000.Google Scholar
  23. [23]
    Pascal Zimmer. Subtyping and typing algorithms for mobile ambients. In FOS-SACS 2000, Berlin, volume 1784 of LNCS, pages 375–390. Springer-Verlag, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Torben Amtoft
    • 1
  • Assaf J. Kfoury
    • 1
  • Santiago M. Pericas-Geertsen
    • 1
  1. 1.Boston UniversityUSA

Personalised recommendations