Abstract
The problem of finding a fully abstract model for the polymorphic π-calculus was stated in Pierce and Sangiorgi’s work in 1997 and has remained open since then. In this paper, we show that a slight variant of their language has a direct 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 conjectured fully abstract model is, in fact, sound but not complete.
Chapter PDF
References
Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)
Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics. North-Holland, Amsterdam (1984)
Berger, M., Honda, K., Yoshida, N.: Genericity and the π-calculus. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 103–119. Springer, Heidelberg (2003)
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)
Canning, P., Cook, W., Hill, W., Olthoff, W., Mitchell, J.C.: F-bounded polymorphism for object-oriented programming. In: Proc. Int. Conf. Functional Programming Languages and Computer Architecture (FPCA), pp. 273–280. ACM Press, New York (1989)
Coppo, M., Dezani-Ciancaglini, M.: A new type-assignment for λ-terms. Archiv Math. Logik 19, 139–156 (1978)
Microsoft Corporation. ECMA and ISO/IEC c# and common language infrastructure standards (2004), http://msdn.microsoft.com/net/ecma/
Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, p. 844. Springer, Heidelberg (1998)
Fournet, C., Gonthier, G., Levy, J.-J., Maranget, L., Remy, D.: A calculus of mobile agents. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)
Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, Cambridge (1989)
Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173(1), 82–120 (2002)
Honda, K., Yoshida, N.: On reduction-based process semantics. Theoretical Computer Science 152(2), 437–486 (1995)
Jeffrey, A.S.A., Rathke, J.: A fully abstract testing semantics for concurrent objects. In: Proc. IEEE Logic In Computer Science, pp. 101–112. IEEE Press, Los Alamitos (2002); Full version to appear in Theoretical Computer Science
Jeffrey, A.S.A., Rathke, J.: Contextual equivalence for higher-order pi-calculus revisited. In: Proc. Mathematical Foundations of Programming Semantics. Electronic Notes in Computer Science. Elsevier, Amsterdam (2003)
Jeffrey, A.S.A., Rathke, J.: Full abstraction for polymorphic pi-calculus. Online edition with proofs (2005), http://www.fabfac.org/
Sun Microsystems. Release notes Java 2 platform standard edition development kit 5.0 (2004), http://java.sun.com/j2se/1.5.0/relnotes.html
Milner, R.: Fully abstract models of typed lambda-calculi. Theoretical Computer Science 4, 1–22 (1977)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R.: Communication and mobile systems: the π-calculus. Cambridge University Press, Cambridge (1999)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Part I + II. Information and Computation 100(1), 1–77 (1992)
Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623. Springer, Heidelberg (1992)
Pierce, B.C., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. J. ACM 47(3), 531–584 (2000)
Pitts, A.M.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10, 321–359 (2000)
Plotkin, G.D.: LCF considered as a programming language. Theoretical Computer Science 5, 223–255 (1977)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. Information Processing 83, 513–523 (1983)
Reynolds, J.C.: An introduction to logical relations and parametric polymorphism (abstract). In: Proc. ACM Symp. Principles of Programming Languages, pp. 155–156. ACM Press, New York (1993)
Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998)
Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh (1993)
Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. In: Proc. ACM Symp. Principles of Programming Languages (2005) (to appear)
Wadler, P.: Theorems for free! In: Proc. Int. Conf. Functional Programming Languages and Computer Architecture (FPCA), pp. 347–359. ACM Press, New York (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jeffrey, A., Rathke, J. (2005). Full Abstraction for Polymorphic Pi-Calculus. In: Sassone, V. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2005. Lecture Notes in Computer Science, vol 3441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31982-5_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-31982-5_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25388-4
Online ISBN: 978-3-540-31982-5
eBook Packages: Computer ScienceComputer Science (R0)