×

zbMATH — the first resource for mathematics

Types and full abstraction for polyadic \(\pi\)-calculus. (English) Zbl 1101.68062
Summary: A type system for terms of the monadic \(\pi\)-calculus is introduced and used to obtain a full-abstraction result for the translation of the polyadic \(\pi\)-calculus into the monadic calculus: well-sorted terms of the polyadic calculus are barbed congruent iff their translations are typed barbed congruent.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.; Gordon, A., A calculus for cryptographic protocols: the spi calculus, Inform. comput., 148, 1-70, (1999) · Zbl 0924.68073
[2] Abramsky, S.; Jagadeesan, R.; Malacaria, P., Full abstraction for PCF, Inform. comput., 163, 2, 409-470, (2000) · Zbl 1006.68028
[3] Boreale, M., On the expressiveness of internal mobility in name-passing calculi, Theoret. comput. sci., 195, 2, 205-226, (1998) · Zbl 0915.68059
[4] G. Boudol, Asynchrony and the π-calculus (note), Rapports de Recherche 1702, INRIA-SOPHIA ANTIPOLIS, 1992.
[5] Fiore, M.; Moggi, E.; Sangiorgi, D., A fully abstract model for the pi-calculus, Inform. comput., 179, 1, 76-117, (2002) · Zbl 1053.68066
[6] C. Fournet, The join-calculus: a calculus for distributed mobile programming, Ph.D. thesis, École Polytechnique, 1998. · Zbl 1065.68071
[7] Hennessy, M.; Riely, J., Information flow vs. resource access in the asynchronous pi-calculus, ACM trans. progr. lang. syst., 24, 5, 566-591, (2002)
[8] Hennessy, M.; Riely, J., Resource access control in systems of mobile agents, Inform. comput., 173, 82-120, (2002) · Zbl 1009.68081
[9] Honda, K.; Tokoro, M., An object calculus for asynchronous communication, ()
[10] Honda, K., Types for dyadic interaction, (), 509-523
[11] Honda, K.; Vasconcelos, V.; Yoshida, N., Secure information flow as typed process behaviour, (), 180-199 · Zbl 0960.68126
[12] K. Honda, N. Yoshida, A uniform type structure for secure information flow, in: Proceedings of the 29th Annual ACM Symposium on Principles of Programming Languages, 2002, pp. 81-92. · Zbl 1323.68375
[13] Hoshina, D.; Sumii, E.; Yonezawa, A., A typed process calculus for finegrained resource access control in distributed computation, (), 6481
[14] Igarashi, A.; Kobayashi, N., Type reconstruction for linear pi-calculus with I/O subtyping, Inform. comput., 161, 1-44, (2000) · Zbl 1046.68620
[15] Igarashi, A.; Kobayashi, N., A generic type system for the pi-calculus, Theoret. comput. sci., 311, 121-163, (2004) · Zbl 1070.68105
[16] N. Kobayashi, B. Pierce, D. Turner, Linearity and the Pi-calculus, in: Proceedings of the 23rd Annual ACM Symposium on Principles of Programming Languages, 1996, pp. 358-371.
[17] N. Kobayashi, A partially deadlock-free typed process calculus, in: Proceedings of the 12th IEEE Symposium on Logic in Computer Science, 1997, pp. 128-139.
[18] M. Merro, D. Sangiorgi, On asynchrony in name-passing calculi, in: Proceedings of the 25th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, Springer, Berlin, 1998. · Zbl 0910.03019
[19] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I and II, Inform. comput., 100, 1, 1-77, (1992)
[20] Milner, R.; Sangiorgi, D., Barbed bisimulation, (), 685-695
[21] R. Milner, Fully abstract models of typed lambda-calculi, Theoret. Comput. Sci. 4 (1977) 1-23. · Zbl 0386.03006
[22] Milner, R., The polyadic π-calculus: a tutorial, (), 203-246
[23] Milner, R., Communicating and mobile systems: the π-calculus, (1999), Cambridge Universtity Press Cambridge · Zbl 0942.68002
[24] Nestmann, U., What is a ‘good’ encoding of guarded choice?, Inform. comput., 156, 287-319, (2000) · Zbl 1046.68625
[25] C. Palamidessi, Comparing the expressive power of the synchronous and the asynchronous π-calculus, in: Proceedings of the 24th Annual ACM Symposium on Principles of Programming Languages, 1997, pp. 256-265.
[26] Pierce, B.; Sangiorgi, D., Typing and subtyping for mobile processes, Math. struct. comput. sci., 6, 5, 409-453, (1996) · Zbl 0861.68030
[27] B. Pierce, D. Sangiorgi, Behavioral equivalence in the polymorphic Pi-calculus, in: Proceedings of the 24th Annual ACM Symposium on Principles of Programming Languages, 1997, pp. 242-255. · Zbl 1094.68591
[28] Quaglia, P.; Walker, D., On encoding in mπ, (), 42-51
[29] Quaglia, P.; Walker, D., On synchronous and asynchronous mobile processes, (), 283-296 · Zbl 0961.68092
[30] J. Riely, M. Hennessy, A typed language for distributed mobile processes, in: Proceedings of the 25th Annual ACM Symposium on Principles of Programming Languages, 1998, pp. 378-390.
[31] Sangiorgi, D., The name discipline of uniform receptiveness, (), 303-313 · Zbl 0930.68035
[32] D. Sangiorgi, Expressing mobility in process algebras: first-order and higher-order paradigms, Ph.D. thesis, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University, report ECS-LFCS-93-266 (1993).
[33] Sangiorgi, D., Lazy functions and mobile processes, () · Zbl 0956.68081
[34] Sangiorgi, D.; Walker, D., The π-calculus: A theory of mobile processes, (2001), Cambridge Universtity Press Cambridge · Zbl 0981.68116
[35] Sewell, P., Global/local subtyping and capability inference for a distributed pi-calculus, (), 695-706 · Zbl 0910.03021
[36] I. Stark, A fully abstract domain model for the Pi-calculus, in: Proceedings of the 11th IEEE Symposium on Logic in Computer Science, 1996, pp. 36-42.
[37] Stoughton, A., Fully abstract models of programming languages, (1988), Pitman London · Zbl 0702.68018
[38] Yoshida, N., Graph types for monadic mobile processes, (), 371-386
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.