Document Open Access Logo

Minimal Session Types (Pearl)

Authors Alen Arslanagić , Jorge A. Pérez , Erik Voogd

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.23.pdf
  • Filesize: 0.65 MB
  • 28 pages

Document Identifiers

Author Details

Alen Arslanagić
  • University of Groningen, The Netherlands
Jorge A. Pérez
  • University of Groningen, The Netherlands
Erik Voogd
  • University of Groningen, The Netherlands

Funding

Work partially supported by the Netherlands Organization for Scientific Research (NWO) under the VIDI Project No. 016.Vidi.189.046 (Unifying Correctness for Communicating Software).

Acknowledgements

We are grateful to the anonymous reviewers for their remarks and questions. Pérez is also with CWI, Amsterdam and NOVA LINCS - the NOVA Laboratory for Computer Science and Informatics, Universidade Nova de Lisboa, Portugal (Ref. UID/CEC/04516/2019).

Cite As Get BibTex

Alen Arslanagić, Jorge A. Pérez, and Erik Voogd. Minimal Session Types (Pearl). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 23:1-23:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ECOOP.2019.23

Abstract

Session types are a type-based approach to the verification of message-passing programs. They have been much studied as type systems for the pi-calculus and for languages such as Java. A session type specifies what and when should be exchanged through a channel. Central to session-typed languages are constructs in types and processes that specify sequencing in protocols.
Here we study minimal session types, session types without sequencing. This is arguably the simplest form of session types. By relying on a core process calculus with sessions and higher-order concurrency (abstraction-passing), we prove that every process typable with standard (non minimal) session types can be compiled down into a process typed with minimal session types. This means that having sequencing constructs in both processes and session types is redundant; only sequentiality in processes is indispensable, as it can precisely codify sequentiality in types.
Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes. By casting Parrow’s results in the realm of typed processes, our results reveal a conceptually simple formulation of session types and a principled avenue to the integration of session types into languages without sequencing in types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Process calculi
  • Software and its engineering → Concurrent programming structures
  • Software and its engineering → Message passing
Keywords
  • Session types
  • process calculi
  • pi-calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages, 3(2-3):95-230, 2016. URL: http://dx.doi.org/10.1561/2500000031.
  2. Stephanie Balzer and Frank Pfenning. Objects as session-typed processes. In Elisa Gonzalez Boix, Philipp Haller, Alessandro Ricci, and Carlos Varela, editors, Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE! 2015, Pittsburgh, PA, USA, October 26, 2015, pages 13-24. ACM, 2015. URL: http://dx.doi.org/10.1145/2824815.2824817.
  3. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In Proc. of PPDP 2012, pages 139-150. ACM, 2012. URL: http://dx.doi.org/10.1145/2370776.2370794.
  4. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. Inf. Comput., 256:253-286, 2017. URL: http://dx.doi.org/10.1016/j.ic.2017.06.002.
  5. Romain Demangeon and Kohei Honda. Full Abstraction in a Subtyped pi-Calculus with Linear Types. In Proc. of CONCUR 2011, volume 6901 of LNCS, pages 280-296. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23217-6_19.
  6. Mariangiola Dezani-Ciancaglini and Ugo de' Liguoro. Sessions and Session Types: an Overview. In WS-FM'09, volume 6194 of LNCS, pages 1-28. Springer, 2010. URL: http://www.di.unito.it/~dezani/papers/sto.pdf.
  7. Mariangiola Dezani-Ciancaglini, Elena Giachino, Sophia Drossopoulou, and Nobuko Yoshida. Bounded Session Types for Object Oriented Languages. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures, volume 4709 of Lecture Notes in Computer Science, pages 207-245. Springer, 2006. URL: http://dx.doi.org/10.1007/978-3-540-74792-5_10.
  8. Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. Session Types for Object-Oriented Languages. In Dave Thomas, editor, ECOOP 2006 - Object-Oriented Programming, 20th European Conference, Nantes, France, July 3-7, 2006, Proceedings, volume 4067 of Lecture Notes in Computer Science, pages 328-352. Springer, 2006. URL: http://dx.doi.org/10.1007/11785477_20.
  9. Simon Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Inf., 42:191-225, 2005. URL: http://dx.doi.org/10.1007/s00236-005-0177-z.
  10. Simon J. Gay, Nils Gesbert, and António Ravara. Session Types as Generic Process Types. In Johannes Borgström and Silvia Crafa, editors, Proceedings Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics, EXPRESS 2014, and 11th Workshop on Structural Operational Semantics, SOS 2014, Rome, Italy, 1st September 2014., volume 160 of EPTCS, pages 94-110, 2014. URL: http://dx.doi.org/10.4204/EPTCS.160.9.
  11. Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, and Alexandre Z. Caldeira. Modular session types for distributed object-oriented programming. In Manuel V. Hermenegildo and Jens Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 299-312. ACM, 2010. URL: http://dx.doi.org/10.1145/1706299.1706335.
  12. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language Primitives and Type Disciplines for Structured Communication-based Programming. In ESOP'98, volume 1381 of LNCS, pages 22-138. Springer, 1998. Google Scholar
  13. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. In POPL'08, pages 273-284. ACM, 2008. Google Scholar
  14. Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-Based Distributed Programming in Java. In Jan Vitek, editor, ECOOP 2008 - Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7-11, 2008, Proceedings, volume 5142 of Lecture Notes in Computer Science, pages 516-541. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70592-5_22.
  15. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv., 49(1):3, 2016. URL: http://dx.doi.org/10.1145/2873052.
  16. Atsushi Igarashi and Naoki Kobayashi. A generic type system for the Pi-calculus. Theor. Comput. Sci., 311(1-3):121-163, 2004. URL: http://dx.doi.org/10.1016/S0304-3975(03)00325-6.
  17. Naoki Kobayashi. Type Systems for Concurrent Programs. In Formal Methods at the Crossroads, volume 2757 of LNCS, pages 439-453. Springer, 2003. URL: http://dx.doi.org/10.1007/978-3-540-40007-3_26.
  18. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking protocols with Mungo and StMungo. In James Cheney and Germán Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, pages 146-159. ACM, 2016. URL: http://dx.doi.org/10.1145/2967973.2968595.
  19. Dimitrios Kouzapas, Jorge A. Pérez, and Nobuko Yoshida. On the Relative Expressiveness of Higher-Order Session Processes. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 446-475. Springer, 2016. Extended version to appear in Information and Computation (Elsevier). URL: http://dx.doi.org/10.1007/978-3-662-49498-1_18.
  20. Dimitrios Kouzapas, Jorge A. Pérez, and Nobuko Yoshida. Characteristic bisimulation for higher-order session processes. Acta Inf., 54(3):271-341, 2017. URL: http://dx.doi.org/10.1007/s00236-016-0289-7.
  21. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A static verification framework for message passing in Go using behavioural types. In Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman, editors, Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, pages 1137-1148. ACM, 2018. URL: http://dx.doi.org/10.1145/3180155.3180157.
  22. Nicholas Ng and Nobuko Yoshida. Static deadlock detection for concurrent go by global session graph synthesis. In Ayal Zaks and Manuel V. Hermenegildo, editors, Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12-18, 2016, pages 174-184. ACM, 2016. URL: http://dx.doi.org/10.1145/2892208.2892232.
  23. Luca Padovani. A Simple Library Implementation of Binary Sessions. Journal of Functional Programming, 27, 2017. URL: http://dx.doi.org/10.1017/S0956796816000289.
  24. Joachim Parrow. Trios in concert. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 623-638. The MIT Press, 2000. Online version, dated July 22, 1996, available at URL: http://user.it.uu.se/~joachim/trios.pdf.
  25. Alceste Scalas and Nobuko Yoshida. Lightweight Session Programming in Scala. In Shriram Krishnamurthi and Benjamin S. Lerner, editors, 30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy, volume 56 of LIPIcs, pages 21:1-21:28. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2016.21.
  26. Vasco T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52-70, 2012. URL: http://dx.doi.org/10.1016/j.ic.2012.05.002.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact