Abstract
Types in processes delineate specific classes of interactive behaviour in a compositional way. Key elements of process theory, in particular behavioural equivalences, are deeply affected by types, leading to applications in the description and analysis of diverse forms of computing. As one of the examples of types for processes, this paper introduces a second-order polymorphic π-calculus based on duality principles, building on type structures coming from typed π-calculi, Linear Logic and game semantics. Of various extensions of first-order typed π-calculi with polymorphism, the present paper focusses on the linear polymorphic π-calculus, extending its first-order counterpart [46]. Fundamental elements of the theory of linear polymorphic processes are studied, including establishment of their strong normalisability using Girard's “candidates,” introduction of a behavioural theory of polymorphic labelled transitions which strengthens Pierce-Sangiorgi's polymorphic bisimulation via duality, and a fully abstract embedding of System F in polymorphic processes, establishing a precise connection between the universe of polymorphic functions and the universe of polymorphic processes. The proof combines process-theoretic reasoning with techniques from game semantics. The abstract nature of polymorphic labelled transitions plays an essential role in full abstraction, elucidating subtle aspects of polymorphism in functions and interaction.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abadi, M., Cardelli, L., Curien, P.-L.: Formal parametric polymorphism. TCS 121,pp. (1–2) 9–58 (1993)
Abramsky, S.: Computational interpretations of linear logic. TCS 111, 3–51 (1993)
Abramsky, S., Jagadeesan, R.: A game semantics for generic polymorphism. In: Proc. FOSSACS'03, no. 2620 in LNCS, pp. 1–22. Springer (2003)
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation 163, 409–470 (2000)
Abramsky, S., Lenisa, M.: Axiomatizing fully complete models for ML polymorphic types. In: Proc. of MFCS'2000, vol. 1893 of LNCS,pp. 141–151. Springer (2000)
Abramsky, S., Lenisa, M.: A fully-complete PER model for ML polymorphic types. In: CSL'2000, vol. 2142 of LNCS, pp. 443–457. Springer (2000)
Barendregt, H.: The Lambda Calculus. North Holland, (1985)
Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T., (eds.) Handbook of Logic in Computer Science. Background: Computational Structures, vol. 2. Clarendon Press (1992)
Berger, M.: Towards Abstractions for Distributed Systems. PhD thesis, Imperial College, London (2002)
Berger, M.: Basic Theory of Reduction Congruence for Two Timed Asynchronous π-Calculi. In: Proc. CONCUR, 3170 pp. 115–13 (2004)
Berger, M., Honda, K., Yoshida, N.: Sequentiality and the π-calculus. Full version of 12
Berger, M., Honda, K., Yoshida, N.: Sequentiality and the π-calculus. In: Proc. TLCA'01, vol. 2044 of LNCS pp. 29–45 (2001)
Berger, M., Honda, K., Yoshida, N.: Genericity and the π-Calculus. In: Proc. FOSSACS'03, no. 2620 in LNCS, pp. 103–119. Springer (2003)
Boudol, G.: Asynchrony and the pi-calculus. Tech. Rep. 1702. INRIA (1992)
Bracha, G., Odersky, M., Stoutamire, D., Wadler, P.: Making the future safe for the past: Adding genericity to the Java programming language. In: Proceedings of ACM OOPSLA 98 (1998)
Girard, J.-Y.: Interprétation Fonctionnelle et Élimination des Coupures de l'Arithmétique d'Ordre Supérieur. PhD thesis, Universite de Paris VII (1972)
Girard, J.-Y.: Linear logic. TCS 50, pp. 1–102 (1987)
Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: Proceedings of ECOOP'91. 512, 133–147 (1991)
Honda, K., Yoshida, N.: Game-Theoretic Analysis of Call-by-Value Computation. TCS 221, 393–456 (1999)
Honda, K., Yoshida, N.: A uniform type structure for secure information flow. In: POPL'02, ACM Press, pp. 81–92 (2002) Full version available at http://www.doc.ic.ac.uk/yoshida
Honda, K., Yoshida, N., Berger, M.: Control in the π-calculus. In: Proc. CW'04, ACM Press (2004)
Hughes, D.J.D.: Games and definability for system F. In: LICS'97, IEEE Computer Society Press, pp. 76–86 (1997)
Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF. Inf. & Comp. 163, 285–408 (2000)
Kleist, J., Sangiorgi, D.: Imperative objects and mobile processes. In: Proc. IFIP Working Conference on Programming Concepts and Methods (PROCOMET'98). North-Holland (1998)
Kobayashi, N., Pierce, B., Turner, D.: Linear types and π-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914–947 (1999)
Lazić, R.S., Newcomb, T., Roscoe, A.: On model checking data-independent systems with arrays without reset. Tech. Rep. RR-02-02, Oxford University (2001)
Milner, R.: Functions as processes. MSCS 2(2), 119–141 (1992)
Milner, R.: The polyadic π-calculus: A tutorial. In: Proceedings of the International Summer School on Logic Algebra of Specification, Marktoberdorf (1992)
Milner, R.: Speech on receiving an Honorary Degree from the University of Bologna, ICALP'97 (1997)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts I and II. Info. & Comp. 100, p. 1 (1992)
Milner, R., Tofte, M., Harper, R.W.: The Definition of Standard ML. MIT Press (1990)
Mitchell, J.C.: On the equivalence of data representation. In: Artificial Intelligence and Mathematical Theory of Computation (1991)
Mitchell, J.C.: Foundations for Programming Languages. MIT Press (1996)
Murawski, A., Ong, C.-H.L.: Evolving games and essential nets for affine polymorphism. In: Proc. of TLCA'01, no. 2044 in LNCS, pp. 360–375. Springer (2001)
Pierce, B., Sangiorgi, D.: Typing and subtyping for mobile processes. MSCS 6(5), 409–454 (1996)
Pierce, B., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. Journal of ACM 47(3), 531–584 (2000)
Pierce, B.C., Turner, D.N.: Pict: A programming language based on the pi-calculus. In: Proof, Language and Interaction: Essays in Honour of Robin Milner, Plotkin, G., Stirling, C., Tofte, M., (eds.) MIT Press (2000)
Pitts, A.M.: Existential Types: Logical Relations and Operational Equivalence. In: Proc. ICALP'98, no. 1443 in LNCS, pp. 309–326 (1998)
Pitts, A.M.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10, 321–359 (2000)
Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: HOOTS'98, CUP, pp. 227–273 (1998)
Plotkin, G., Abadi, M.: A logic for parameteric polymorphism. In: LICS'98, IEEE Press, pp. 42–53 (1998)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Information Processing. Mason, R.E.A.(ed.) 83 (1983)
Turner, D.N.: The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh (1996)
Vasconcelos, V.T.: Typed Concurrent Objects. In: 8th ECOOP, vol. 821 of Lecture Notes in Computer Science, pp. 100–117 (1994)
Vasconcelos, V.T., Honda, K.: Principal typing-schemes in a polyadic π-calculus. In: 4th CONCUR, vol. 715 of Lecture Notes in Computer Science, pp. 524–538 (1993)
Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the π-Calculus. In: LICS'01, IEEE, pp. 311–322 (2001) The full version in Journal of Inf. & Comp. 191, 145–202 Elsevier (2004)
Yoshida, N., Honda, K., Berger, M.: Linearity and bisimulation. In: FoSSaCs02, vol. 2303 of LNCS, pp.417–433. Springer (2002)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Berger, M., Honda, K. & Yoshida, N. Genericity and the π-calculus. Acta Informatica 42, 83–141 (2005). https://doi.org/10.1007/s00236-005-0175-1
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00236-005-0175-1