zbMATH — the first resource for mathematics

Full abstraction for polymorphic \(\pi \)-calculus. (English) Zbl 1134.68040
Summary: The problem of finding a fully abstract model for the polymorphic \(\pi \)-calculus was stated in B. C. Pierce and D. Sangiorgi’s work in [J. ACM 47, No. 3, 531–584 (2000; Zbl 1094.68591)] and has remained open since then. In this paper, we show that a variant of their language has a fully abstract model, which does not depend on type unification or logical relations. This is the first fully abstract model for a polymorphic concurrent language. In addition, we discuss the relationship between our work and Pierce and Sangiorgi’s, and show that their model based on type unification is sound but not complete.
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI
[1] Abadi, M.; Cardelli, L., A theory of objects, (1996), Springer-Verlag · Zbl 0876.68014
[2] Barendregt, H.P., The lambda calculus, its syntax and semantics, (1984), North-Holland · Zbl 0551.03007
[3] Berger, M.; Honda, K.; Yoshida, N., Genericity and the \(\pi\)-calculus, () · Zbl 1029.68039
[4] Brookes, S.D.; Hoare, C.A.R.; Roscoe, A.W., A theory of communicating sequential processes, Journal of the ACM, 31, 3, 560-599, (1984) · Zbl 0628.68025
[5] Canning, P.; Cook, W.; Hill, W.; Olthoff, W.; Mitchell, J.C., F-bounded polymorphism for object-oriented programming, (), 273-280
[6] Coppo, M.; Dezani-Ciancaglini, M., A new type-assignment for \(\lambda\)-terms, Archive for mathematical logic, 19, 139-156, (1978) · Zbl 0418.03010
[7] Microsoft Corporation, ECMA and ISO/IEC C# and common language infrastructure standards, 2004. http://msdn.microsoft.com/net/ecma/
[8] Fournet, C.; Gonthier, G., A hierarchy of equivalences for asynchronous calculi, () · Zbl 1066.68088
[9] Fournet, C.; Gonthier, G.; Levy, J.-J.; Maranget, L.; Remy, D., A calculus of mobile agents, ()
[10] Girard, J.-Y.; Taylor, P.; Lafont, Y., Proofs and types, (1989), Cambridge University Press
[11] Hennessy, M., Algebraic theory of processes, (1988), MIT Press · Zbl 0744.68047
[12] Hennessy, M.; Riely, J., Resource access control in systems of mobile agents, Information and computation, 173, 1, 82-120, (2002) · Zbl 1009.68081
[13] Honda, K.; Yoshida, N., On reduction-based process semantics, Theoretical computer science, 152, 2, 437-486, (1995) · Zbl 0871.68122
[14] Jeffrey, A.S.A.; Rathke, J., A fully abstract may testing semantics for concurrent objects, (), 101-112, Full version to appear in Theoretical Computer Science
[15] Jeffrey, A.S.A.; Rathke, J., Contextual equivalence for higher-order \(\pi\)-calculus revisited, () · Zbl 1337.68185
[16] Sun Microsystems, Release notes Java 2 platform standard edition development kit 5.0, 2004. http://java.sun.com/j2se/1.5.0/relnotes.html
[17] Milner, R., Fully abstract models of typed lambda-calculi, Theoretical computer science, 4, 1-22, (1977) · Zbl 0386.03006
[18] Milner, R., Communication and concurrency, (1989), Prentice-Hall · Zbl 0683.68008
[19] Milner, R., Communication and mobile systems: the \(\pi\)-calculus, (1999), Cambridge University Press · Zbl 0942.68002
[20] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I + II, Information and computation, 100, 1, 1-77, (1992)
[21] Milner, R.; Sangiorgi, D., Barbed bisimulation, ()
[22] Pierce, B.C.; Sangiorgi, D., Behavioral equivalence in the polymorphic \(\pi\)-calculus, Journal of the ACM, 47, 3, 531-584, (2000) · Zbl 1094.68591
[23] Pitts, A.M., Parametric polymorphism and operational equivalence, Mathematical structures in computer science, 10, 321-359, (2000) · Zbl 0955.68024
[24] Plotkin, G.D., LCF considered as a programming language, Theoretical computer science, 5, 223-255, (1977) · Zbl 0369.68006
[25] Reynolds, J.C., Types, abstraction and parametric polymorphism, Information processing, 83, 513-523, (1983)
[26] Reynolds, J.C., An introduction to logical relations and parametric polymorphism (abstract), (), 155-156
[27] Reynolds, J.C., Theories of programming languages, (1998), Cambridge University Press · Zbl 0972.68507
[28] Sangiorgi, D.; Walker, D., The pi-calculus: A theory of mobile processes, (2001), Cambridge University Press · Zbl 0981.68116
[29] E. Sumii, B.C. Pierce, A bisimulation for type abstraction and recursion, in: Proc. ACM Symp. Principles of Programming Languages, 2005, pp. 63-74 · Zbl 1369.68117
[30] Wadler, P., Theorems for free!, (), 347-359
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.