Skip to main content
SpringerLink
Log in
Book cover

Processes, Terms and Cycles: Steps on the Road to Infinity pp 404–444Cite as

A Mobility Calculus with Local and Dependent Types

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3838))

Abstract

We introduce an ambient-based calculus that combines ambient mobility with process mobility, uses group names to collect ambients with homologous features, and exploits co-moves and runtime type checking to implement flexible policies for controlling process activities. Types rely on group names and, to support dynamicity, may depend on group variables. Policies can dynamically change also through installation of co-moves. The compliance with ambient policies can be checked locally to the ambients and requires no global assumptions. We prove that the type assignment system and the operational semantics of the calculus are ‘sound’, and define a sound and complete type inference algorithm which, when applied to terms whose type decorations only express the desired policies, computes the minimal type annotations required for their execution. As an application of our calculus, we present a couple of examples and linger on the setting up of policies for controlling the activities of the entities involved.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Amtoft, T., Kfoury, A.J., Pericas-Geertsen, S.M.: What are Polymorphically-Typed Ambients? In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 206–220. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  2. Barbanera, F., Dezani-Ciancaglini, M., Salvo, I., Sassone, V.: A type inference algorithm for secure ambients. In: Lenisa, M., Miculan, M. (eds.) Proc. of TOSCA 2001. ENTCS, vol. 62. Elsevier Science, Amsterdam (2002)

    Google Scholar 

  3. Bettini, L., Bono, V., Nicola, R.D., Ferrari, G., Gorla, D., Loreti, M., Moggi, E., Pugliese, R., Tuosto, E., Venneri, B.: The KLAIM Project: Theory and Practice. In: Priami, C. (ed.) GC 2003. LNCS, vol. 2874, pp. 88–151. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Bonelli, E., Compagnoni, A., Dezani-Ciancaglini, M., Garralda, P.: Boxed Ambients with Communication Interfaces. In: Fiala, J., Koubek, V., Kratochvíl, J. (eds.) MFCS 2004. LNCS, vol. 3153, pp. 119–148. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Boudol, G.: A Parametric Model of Migration and Mobility, Release 1. Mikado Deliverable D1.2.1 (2003), available at, http://mikado.di.fc.ul.pt/repository/D1.2.1.pdf

  6. Bugliesi, M., Castagna, G.: Behavioral Typing for Safe Ambients. Computer Languages 28(1), 61–99 (2002)

    MATH  Google Scholar 

  7. Bugliesi, M., Castagna, G., Crafa, S.: Access Control for Mobile Agents: The Calculus of Boxed Ambients. ACM Transactions on Programming Languages and Systems 26(1), 57–124 (2004)

    Article  Google Scholar 

  8. Bugliesi, M., Crafa, S., Merro, M., Sassone, V.: Communication and Mobility Control in Boxed Ambients. Information and Computation 202(1), 39–86 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  9. Cardelli, L.: Abstractions for Mobile Computation. In: Vitek, J. (ed.) Secure Internet Programming. LNCS, vol. 1603, pp. 51–94. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Cardelli, L., Ghelli, G., Gordon, A.D.: Mobility Types for Mobile Ambients. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 230–239. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  11. Cardelli, L., Ghelli, G., Gordon, A.D.: Types for the Ambient Calculus. Information and Computation 177(2), 160–194 (2002)

    MATH  MathSciNet  Google Scholar 

  12. Cardelli, L., Gordon, A.D.: Mobile Ambients. Theoretical Computer Science 240(1), 177–213 (2000); Special Issue on Coordination, Daniel Le Métayer Editor

    Article  MATH  MathSciNet  Google Scholar 

  13. Castagna, G., Vitek, J., Nardelli, F.Z.: The Seal Calculus. Information and Computation 201(1), 1–54 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  14. Coppo, M., Dezani-Ciancaglini, M., Giovannetti, E., Pugliese, R.: Dynamic and Local Typing for Mobile Ambients. In: Proc. of TCS 2004, pp. 583–596. Kluwer, Dordrecht (2004)

    Google Scholar 

  15. Coppo, M., Dezani-Ciancaglini, M., Giovannetti, E., Salvo, I.: M3: Mobility Types for Mobile Processes in Mobile Ambients. In: Harland, J. (ed.) Proc. of CATS 2003. ENTCS, vol. 78. Elsevier, Amsterdam (2003)

    Google Scholar 

  16. Curry, H.B., Feys, R.: Combinatory Logic. Studies in Logic and the Foundations of Mathematics, vol. I. North-Holland, Amsterdam (1958)

    MATH  Google Scholar 

  17. De Nicola, R., Ferrari, G., Pugliese, R.: Klaim: a Kernel Language for Agents Interaction and Mobility. IEEE Transactions on Software Engineering 24(5), 315–330 (1998)

    Article  Google Scholar 

  18. De Nicola, R., Gorla, D., Pugliese, R.: Basic observables for a calculus for global computing. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1226–1238. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Ferrari, G., Moggi, E., Pugliese, R.: Guardians for Ambient-based Monitoring. In: Sassone, V. (ed.) Proc. of F-WAN. ENTCS, vol. 66. Elsevier, Amsterdam (2002)

    Google Scholar 

  20. Francalanza, A., Hennessy, M.: A theory of system behaviour in the presence of node and link failures. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 368–382. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  21. Giovannetti, E.: Ambient Calculi with Types: a Tutorial. In: Priami, C. (ed.) GC 2003. LNCS, vol. 2874, pp. 151–191. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  22. Goguen, H.: Typed Operational Semantics. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 186–200. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  23. Gorla, D., Hennessy, M., Sassone, V.: Security Policies as Membranes in Systems for Global Computing. In: Rathke, J. (ed.) Proc. of FGUC 2004. ENTCS. Elsevier, Amsterdam (2004)

    Google Scholar 

  24. Gorla, D., Pugliese, R.: Resource Acces and Mobility Control with Dynamic Privileges Acquisition. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 119–132. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  25. Hennessy, M., Rathke, J., Yoshida, N.: SafeDpi: A language for controlling mobile code (extended abstract). In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 241–256. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  26. Hennessy, M., Riely, J.: Type-Safe Execution of Mobile Agents in Anonymous Networks. In: Vitek, J. (ed.) Secure Internet Programming. LNCS, vol. 1603, pp. 95–115. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  27. Hennessy, M., Riely, J.: Resource Access Control in Systems of Mobile Agents. Information and Computation 173, 82–120 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  28. Hennessy, M., Riely, J.: Trust and Partial Typing in Open Systems of Mobile Agents. Journal of Automated Reasoning 31(3-4), 335–370 (2003)

    MATH  MathSciNet  Google Scholar 

  29. Levi, F., Sangiorgi, D.: Controlling Interference in Ambients. Transactions on Programming Languages and Systems 25(1), 1–69 (2003)

    Article  Google Scholar 

  30. Lhoussaine, C., Sassone, V.: A Dependently Typed Ambient Calculus. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 171–187. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  31. Merro, M., Hennessy, M.: Bisimulation Congruences in Safe Ambients. In: Jones, N.D., Leroy, X. (eds.) Proc. of POPL 2002, pp. 71–80. ACM Press, New York (2002)

    Google Scholar 

  32. Merro, M., Sassone, V.: Typing and Subtyping Mobility in Boxed Ambients. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 304–320. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  33. Necula, G.C.: Proof-Carrying Code. In: Jones, N.D. (ed.) Proc. of POPL 1997, pp. 106–119. ACM Press, New York (1997)

    Chapter  Google Scholar 

  34. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    Google Scholar 

  35. Pierce, B.C., Sangiorgi, D.: Typing and Subtyping for Mobile Processes. Mathematical Structures in Computer Science 6(5), 409–454 (1996); An extract appeared in Proc. of LICS 1993, pp. 376–385 (1993)

    MATH  MathSciNet  Google Scholar 

  36. Zimmer, P.: Subtyping and typing algorithms for mobile ambients. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 375–390. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dip. Informatica, Univ. di Torino, corso Svizzera 185, Torino, Italy

    Mario Coppo, Mariangiola Dezani-Ciancaglini & Elio Giovannetti

  2. Dip. Scienze Matematiche e Informatiche, Univ. di Siena, pian dei Mantellini 44, Siena, Italy

    Federico Cozzi

  3. Dip. Sistemi e Informatica, Univ. di Firenze, viale Morgagni 65, Firenze, Italy

    Rosario Pugliese

Authors
  1. Mario Coppo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Federico Cozzi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mariangiola Dezani-Ciancaglini
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Elio Giovannetti
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Rosario Pugliese
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, Austria

    Aart Middeldorp

  2. Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS, Utrecht, The Netherlands

    Vincent van Oostrom

  3. Department of Theoretical Computer Science, Vrije Universiteit, De Boelelaan 1081a, 1081 HV, Amsterdam, The Netherlands

    Femke van Raamsdonk

  4. VU Vrije Universiteit Amsterdam,  

    Roel de Vrijer

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Coppo, M., Cozzi, F., Dezani-Ciancaglini, M., Giovannetti, E., Pugliese, R. (2005). A Mobility Calculus with Local and Dependent Types. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds) Processes, Terms and Cycles: Steps on the Road to Infinity. Lecture Notes in Computer Science, vol 3838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11601548_20

Download citation

  • DOI: https://doi.org/10.1007/11601548_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-30911-6

  • Online ISBN: 978-3-540-32425-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation