Advertisement

Polymorphic Session Processes as Morphisms

  • Bernardo ToninhoEmail author
  • Nobuko Yoshida
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11760)

Abstract

The study of expressiveness of concurrent processes via session types opens a connection between linear logic and mobile processes, grounded in the rigorous logical background of propositions-as-types. One such study includes a notion of parametric session polymorphism, which connects session typed processes with rich higher-order functional computations. This work proposes a novel and non-trivial application of session parametricity – an encoding of inductive and coinductive session types, justified via the theory of initial algebras and final co-algebras using a processes-as-morphisms viewpoint. The correctness of the encoding (i.e. universality) relies crucially on parametricity and the associated relational lifting of sessions.

Keywords

Expressiveness Session types \(\pi \)-calculus F-Algebra Linear logic 

Notes

Acknowledgements

The authors would like to thank Dominic Orchard and the anonymous reviewers for their comments and suggestions. This work is partially supported by EPSRC EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1 and NOVA LINCS (UID/CEC/04516/2019).

References

  1. 1.
    Bainbridge, E.S., Freyd, P.J., Scedrov, A., Scott, P.J.: Functorial polymorphism. Theor. Comput. Sci. 70(1), 35–64 (1990)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall Inc., Upper Saddle River (1997)zbMATHGoogle Scholar
  3. 3.
    Bird, R.S., de Moor, O., Hoogendijk, P.F.: Generic functional programming with types and relations. J. Funct. Program. 6(1), 1–28 (1996)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Linear Abadi and Plotkin Logic. Logical Methods Comput. Sci. 2(5) (2006). https://lmcs.episciences.org/2233
  5. 5.
    Caires, L., Pérez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 330–349. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_19CrossRefzbMATHGoogle Scholar
  6. 6.
    Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15375-4_16CrossRefGoogle Scholar
  7. 7.
    Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Math. Struct. Comput. Sci. 26(3), 367–423 (2016)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Girard, J.: Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination de coupures dans l’analyse et la théorie des types. In: Proceedings of the 2nd Scandinavian Logic Symposium, pp. 63–92 (1971)CrossRefGoogle Scholar
  9. 9.
    Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Girard, J., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)zbMATHGoogle Scholar
  11. 11.
    Hasegawa, R.: Categorical data types in parametric polymorphism. Math. Struct. Comput. Sci. 4(1), 71–109 (1994)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Hodas, J., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110, 327–365 (1994)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0053567CrossRefGoogle Scholar
  14. 14.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL 2008, pp. 273–284 (2008)CrossRefGoogle Scholar
  15. 15.
    Lindley, S., Morris, J.G.: Talking bananas: structural recursion for session types. In: ICFP 2016, pp. 434–447 (2016)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Mendler, N.P.: Recursive types and type constraints in second-order lambda calculus. In: LICS, pp. 30–36 (1987)Google Scholar
  17. 17.
    Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Logic Comput. 1(4), 497–536 (1991)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic 51, 125–157 (1991)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Palamidessi, C.: Comparing the expressive power of the synchronous and the asynchronous \(\pi \)-calculus. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 256–265. ACM, New York (1997)Google Scholar
  20. 20.
    Palamidessi, C.: Comparing the expressive power of the synchronous and asynchronous \(\pi \)-calculi. Math. Struct. Comput. Sci. 13(5), 685–719 (2003)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Pérez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear logical relations for session-based concurrency. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 539–558. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28869-2_27CrossRefGoogle Scholar
  22. 22.
    Pierce, B.C., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. J. ACM 47(3), 531–584 (2000)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361–375. Springer, Heidelberg (1993).  https://doi.org/10.1007/BFb0037118CrossRefGoogle Scholar
  24. 24.
    Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513–523 (1983)Google Scholar
  25. 25.
    Sangiorgi, D.: Pi-calculus, internal mobility, and agent-passing calculi. Theor. Comput. Sci. 167(1&2), 235–274 (1996)CrossRefGoogle Scholar
  26. 26.
    Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  27. 27.
    Toninho, B., Caires, L., Pfenning, F.: Functions as session-typed processes. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 346–360. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28729-9_23CrossRefGoogle Scholar
  28. 28.
    Toninho, B., Caires, L., Pfenning, F.: Corecursion and non-divergence in session-typed processes. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 159–175. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-45917-1_11CrossRefGoogle Scholar
  29. 29.
    Toninho, B., Yoshida, N.: On polymorphic sessions and functions. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 827–855. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89884-1_29CrossRefzbMATHGoogle Scholar
  30. 30.
    Toninho, B., Yoshida, N.: Polymorphic session processes as morphisms. Technical report 02/2019, Department of Computing, Imperial College London, July 2019. https://www.doc.ic.ac.uk/research/technicalreports/2019/DTRS19-2.pdf
  31. 31.
  32. 32.
    Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2–3), 384–418 (2014)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Zhao, J., Zhang, Q., Zdancewic, S.: Relational parametricity for a polymorphic linear lambda calculus. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 344–359. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17164-2_24CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Universidade Nova de Lisboa and NOVA-LINCSLisbonPortugal
  2. 2.Imperial College LondonLondonUK

Personalised recommendations