What Are Polymorphically-Typed Ambients?
The Ambient Calculus was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code . 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 .
KeywordsDenotational Semantic Conservative Extension Type Check Trace Semantic Subject Reduction
- 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
- Torben Amtoft, Flemming Nielson, and Hanne Riis Nielson. Type and Effect Systems: Behaviours for Concurrency. Imperial College Press, 1999.Google Scholar
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- Francesca Levi and Davide Sangiorgi. Controlling interference in ambients. In POPL’00, Boston, Massachusetts, pages 352–364. ACM Press, January 2000.Google Scholar
- 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.Google Scholar
- Benjamin C. Pierce and David N. Turner. Pict: A programming language based on the pi-calculus. Technical report, IU, 1997.Google Scholar
- 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
- 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
- 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
- David N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh, 1995. Report no ECS-LFCS-96-345.Google Scholar
- 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
- 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
- Nobuko Yoshida and Matthew Hennessy. Assigning types to processes. In LICS 2000, pages 334–345, 2000.Google Scholar
- 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