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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Abadi, M.: Secrecy by typing in security protocols. J. ACM 46(5), 749–786 (1999)
Abadi, M., Blanchet, B.: Secrecy types for asymmetric communication. Theor. Comput. Sci. 298(3), 387–415 (2003)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. In: Proc. CCS 1997, pp. 36–47. ACM, New York (1997)
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)
Carbone, M., Maffeis, S.: On the expressive power of polyadic synchronisation in π-calculus. Nordic Journal of Computing 10(2), 70–98 (2003)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, p. 140. Springer, Heidelberg (1998)
Deng, Y., Sangiorgi, D.: Ensuring termination by typability. Inf. Comput. 204(7), 1045–1082 (2006)
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)
Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. 29(5) (2007)
Gabbay, M.J., Mathijssen, A.: Nominal (universal) algebra: Equational logic with names and binding. J. Log. Comput. 19(6), 1455–1508 (2009)
Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. J. Comput. Secur. 11(4), 451–519 (2003)
Honda, K.: Composing processes. In: Proc. of POPL 1996, pp. 344–357. ACM, New York (1996)
Igarashi, A., Kobayashi, N.: A generic type system for the Pi-calculus. Theor. Comput. Sci. (11), 121–163 (2004)
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914–947 (1999)
Kobayashi, N., Sangiorgi, D.: A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst. 32(5) (2010)
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)
Milner, R.: The polyadic pi-calculus: a tutorial, pp. 203–246. Springer, Heidelberg (1993)
Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press, Cambridge (2009)
Pierce, B.C., Sangiorgi, D.: Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6(5), 409–453 (1996)
Riely, J., Hennessy, M.: A typed language for distributed mobile processes. In: Proceedings of POPL 1998, pp. 378–390. ACM, New York (1998)
Riely, J., Hennessy, M.: Trust and partial typing in open systems of mobile agents. J. Autom. Reasoning 31(3-4), 335–370 (2003)
Sangiorgi, D.: The name discipline of uniform receptiveness. Theor. Comput. Sci. 221(1-2), 457–493 (1999)
Sangiorgi, D., Walker, D.: The π-Calculus - A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Wischik, L., Gardner, P.: Explicit fusions. Theor. Comput. Sci. 340(3), 606–630 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)