Skip to main content
SpringerLink
Log in

Typed ψ-calculi

  • Conference paper
CONCUR 2011 – Concurrency Theory (CONCUR 2011)

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

Included in the following conference series:

Abstract

A large variety of process calculi extend the π-calculus with more general notions of messages. Bengtson et al. have shown that many of these π-like calculi can be expressed as so-called ψ-calculi. In this paper, we describe a simple type system for ψ-calculi. The type system satisfies a subject reduction property and a general notion of channel safety. A number of existing systems are shown to be instances of our system, and other, new type systems can also be obtained. We first present a new type system for the calculus of explicit fusions by Wischik and Gardner, then one for the distributed π-calculus of Hennessy and Riely and finally show how existing type systems for secrecy and authenticity in the spi calculus can be represented and shown to be safe.

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

Access this chapter

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 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. Abadi, M.: Secrecy by typing in security protocols. J. ACM 46(5), 749–786 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  2. Abadi, M., Blanchet, B.: Secrecy types for asymmetric communication. Theor. Comput. Sci. 298(3), 387–415 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  3. Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. In: Proc. CCS 1997, pp. 36–47. ACM, New York (1997)

    Google Scholar 

  4. Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: Mobile Processes, Nominal Data, and Logic. In: Proc. of LICS 2009, pp. 39–48. IEEE, Los Alamitos (2009)

    Google Scholar 

  5. Carbone, M., Maffeis, S.: On the expressive power of polyadic synchronisation in π-calculus. Nordic Journal of Computing 10(2), 70–98 (2003)

    MathSciNet  MATH  Google Scholar 

  6. Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, p. 140. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  7. Deng, Y., Sangiorgi, D.: Ensuring termination by typability. Inf. Comput. 204(7), 1045–1082 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  8. Elsborg, E., Hildebrandt, T., Sangiorgi, D.: Type systems for bigraphs. In: Kaklamanis, C., Nielson, F. (eds.) TGC 2008. LNCS, vol. 5474, pp. 126–140. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. 29(5) (2007)

    Google Scholar 

  10. Gabbay, M.J., Mathijssen, A.: Nominal (universal) algebra: Equational logic with names and binding. J. Log. Comput. 19(6), 1455–1508 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  11. Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. J. Comput. Secur. 11(4), 451–519 (2003)

    Article  Google Scholar 

  12. Honda, K.: Composing processes. In: Proc. of POPL 1996, pp. 344–357. ACM, New York (1996)

    Google Scholar 

  13. Igarashi, A., Kobayashi, N.: A generic type system for the Pi-calculus. Theor. Comput. Sci. (11), 121–163 (2004)

    Google Scholar 

  14. Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914–947 (1999)

    Article  Google Scholar 

  15. Kobayashi, N., Sangiorgi, D.: A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst. 32(5) (2010)

    Google Scholar 

  16. Makholm, H., Wells, J.B.: Instant polymorphic type systems for mobile process calculi: Just add reduction rules and close. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 389–407. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  17. Milner, R.: The polyadic pi-calculus: a tutorial, pp. 203–246. Springer, Heidelberg (1993)

    Google Scholar 

  18. Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press, Cambridge (2009)

    Book  MATH  Google Scholar 

  19. Pierce, B.C., Sangiorgi, D.: Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6(5), 409–453 (1996)

    MathSciNet  MATH  Google Scholar 

  20. Riely, J., Hennessy, M.: A typed language for distributed mobile processes. In: Proceedings of POPL 1998, pp. 378–390. ACM, New York (1998)

    Google Scholar 

  21. Riely, J., Hennessy, M.: Trust and partial typing in open systems of mobile agents. J. Autom. Reasoning 31(3-4), 335–370 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  22. Sangiorgi, D.: The name discipline of uniform receptiveness. Theor. Comput. Sci. 221(1-2), 457–493 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  23. Sangiorgi, D., Walker, D.: The π-Calculus - A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)

    MATH  Google Scholar 

  24. Wischik, L., Gardner, P.: Explicit fusions. Theor. Comput. Sci. 340(3), 606–630 (2005)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, Denmark

    Hans Hüttel

Authors
  1. Hans Hüttel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Software Modeling and Verification, RWTH Aachen, Ahornstraße 55, 52074, Aachen, Germany

    Joost-Pieter Katoen

  2. Fakultät für Ingenieurwesen, Abteilung für Informatik und Angewandte Kognitionswissenschaft, Universität Duisburg-Essen,, Lotharstraße 65, 47057, Duisburg, Germany

    Barbara König

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hüttel, H. (2011). Typed ψ-calculi. In: Katoen, JP., König, B. (eds) CONCUR 2011 – Concurrency Theory. CONCUR 2011. Lecture Notes in Computer Science, vol 6901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23217-6_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-23217-6_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-23216-9

  • Online ISBN: 978-3-642-23217-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation