Skip to main content

Types for Evolving Communication in Safe Ambients

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2575))

Abstract

We extend the evolving types of [10] to full Safe Ambients following the lines of the single-threaded types of [12] for communication. Then, we introduce more flexible evolving types which permit to define ambients, where the type of the exchanged data may vary as the internal computation proceeds or after the ambient is opened.

There is an obvious encoding of MA into SA.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Torben Amtoft and Assaf J. Kfoury and Santiago M. Pericas-Geertsen. What are Polymorphically-Typed Ambients? In Proc. ESOP’01, volume 2028 of Lecture Notes in Computer Science, pages 206–220. Springer Verlag, 2001.

    Google Scholar 

  2. Torben Amtoft and Assaf J. Kfoury and Santiago M. Pericas-Geertsen. Orderly Communication in the Ambient Calculus. To appear in Computer Languages.

    Google Scholar 

  3. M. Bugliesi and G. Castagna. Secure safe ambients. In Proc. POPL’ 01, pages 222–235. ACM Press, 2001.

    Google Scholar 

  4. L. Cardelli, G. Ghelli, and A.D. Gordon. Mobility types for mobile ambients. In Proc. ICALP’99, volume 1644 of Lecture Notes in Computer Science, pages 230–239. Springer Verlag, 1999.

    Google Scholar 

  5. L. Cardelli and A.D. Gordon. Mobile ambients. In Proc. FoSSaCS’ 98, volume 1378 of Lecture Notes in Computer Science, pages 140–155. Springer Verlag, 1998.

    Google Scholar 

  6. L. Cardelli and A.D. Gordon. Types for mobile ambients. In Proc. POPL’99, pages 79–92. ACM Press, 1999.

    Google Scholar 

  7. L. Cardelli, G. Ghelli, and A.D. Gordon. Types for ambient calculus. To apper in Information and Computation.

    Google Scholar 

  8. P. Degano, F. Levi and C. Bodei. Safe Ambients: Control Flow Analysis and Security. In Proc. ASIAN’ 00, volume 1961 of Lecture Notes in Computer Science, pages 199–214. Springer Verlag, 2000.

    Google Scholar 

  9. M. Dezani-Ciancaglini and I. Salvo. Security Types for Mobile Safe Ambients. In Proc. ASIAN’ 00, volume 1961 of Lecture Notes in Computer Science, pages 215–236. Springer Verlag, 2000.

    Google Scholar 

  10. X. Guan, Y. Yang, and J. You. Typing Evolving Ambients. Information Processing Letters, 80(5), 265–270, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  11. F. Levi. Types for Evolving Communication in Safe Ambients (Draft). Available at http://www.di.unipi.it/∼levifran/papers.html.

  12. F. Levi and D. Sangiorgi. Controlling Interference in Ambients. In Proc. POPL’ 00, pages 352–364. ACM Press, 2000.

    Google Scholar 

  13. M. Merro and M. Hennessy. Bisimulation congruences in Safe Ambients. In Proc. POPL’ 02. ACM Press, 2002.

    Google Scholar 

  14. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, (Parts I and II). Information and Computation, 100:1–77, 1992.

    MATH  MathSciNet  Google Scholar 

  15. P. Zimmer Subtyping and typing algorithms for mobile ambients. In Proc. FOSSACS’ 00, volume 1784 of Lecture Notes in Computer Science, pages 375–390. Springer Verlag, 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Levi, F. (2003). Types for Evolving Communication in Safe Ambients. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2003. Lecture Notes in Computer Science, vol 2575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36384-X_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-36384-X_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00348-9

  • Online ISBN: 978-3-540-36384-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics