Skip to main content
SpringerLink
Log in

A Session Subtyping Tool

  • Conference paper
  • First Online:
Coordination Models and Languages (COORDINATION 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12717))

Included in the following conference series:

Abstract

Session types are becoming popular and have been integrated in several mainstream programming languages. Nevertheless, while many programming languages consider asynchronous fifo channel communication, the notion of subtyping used in session type implementations is the one defined by Gay and Hole for synchronous communication. This might be because there are several notions of asynchronous session subtyping, these notions are usually undecidable, and only recently sound (but not complete) algorithmic characterizations for these subtypings have been proposed. But the fact that the definition of asynchronous session subtyping and the theory behind related algorithms are not easily accessible to non-experts may also prevent further integration. The aim of this paper, and of the tool presented therein, is to make the growing body of knowledge about asynchronous session subtyping more accessible, thus promoting its integration in practical applications of session types.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    As we will see, the order in which the LTSs are presented reflects the subtyping relation (we will show that \(T''_{HC}\) and \(T'_{HC}\) are subtypes of \(T_{HC}\)) and the positions in which types are inputed in the tool.

References

  1. Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2–3), 95–230 (2016)

    Article  Google Scholar 

  2. Bacchiani, L., Bravetti, M., Lange, J., Zavattaro, G.: Tool source files for Linux, Windows and OSx (and binaries for Windows and OSx). https://github.com/LBacchiani/session-subtyping-tool

  3. Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)

    Article  MathSciNet  Google Scholar 

  4. Bravetti, M.: Axiomatizing maximal progress and discrete time. Log. Methods Comput. Sci. 17(1), 1:1–1:44 (2021)

    Google Scholar 

  5. Bravetti, M., Carbone, M., Lange, J., Yoshida, N., Zavattaro, G.: A sound algorithm for asynchronous session subtyping and its implementation. Log. Methods Comput. Sci. 17(1), 20:1–20:35 (2021)

    Google Scholar 

  6. Bravetti, M., Carbone, M., Zavattaro, G.: Undecidability of asynchronous session subtyping. Inf. Comput. 256, 300–320 (2017)

    Article  MathSciNet  Google Scholar 

  7. Bravetti, M., Carbone, M., Zavattaro, G.: On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci. 722, 19–51 (2018)

    Article  MathSciNet  Google Scholar 

  8. Bravetti, M., et al.: Behavioural types for memory and method safety in a core object-oriented language. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 105–124. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-64437-6_6

    Chapter  Google Scholar 

  9. Bravetti, M., Lange, J., Zavattaro, G.: Fair refinement for asynchronous session types. In: Kiefer, S., Tasson, C. (eds.) FOSSACS 2021. LNCS, vol. 12650, pp. 144–163. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-71995-1_8

    Chapter  Google Scholar 

  10. Bravetti, M., Zavattaro, G.: On the expressive power of process interruption and compensation. Math. Struct. Comput. Sci. 19(3), 565–599 (2009)

    Article  MathSciNet  Google Scholar 

  11. Bravetti, M., Zavattaro, G.: Asynchronous session subtyping as communicating automata refinement. Softw. Syst. Model. 20(2), 311–333 (2020). https://doi.org/10.1007/s10270-020-00838-x

    Article  Google Scholar 

  12. Chen, T., Dezani-Ciancaglini, M., Scalas, A., Yoshida, N.: On the preciseness of subtyping in session types. Log. Methods Comput. Sci. 13(2), 1–61 (2017)

    MathSciNet  MATH  Google Scholar 

  13. Deniélou, P.-M., Yoshida, N.: Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 174–186. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39212-2_18

    Chapter  MATH  Google Scholar 

  14. Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42(2–3), 191–225 (2005)

    Article  MathSciNet  Google Scholar 

  15. Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 401–418. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_24

    Chapter  Google Scholar 

  16. Kozen, D., Palsberg, J., Schwartzbach, M.I.: Efficient recursive subtyping. Math. Struct. Comput. Sci. 5(1), 113–125 (1995)

    Article  MathSciNet  Google Scholar 

  17. Lange, J., Yoshida, N.: Characteristic formulae for session types. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 833–850. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_52

    Chapter  MATH  Google Scholar 

  18. Lange, J., Yoshida, N.: On the undecidability of asynchronous session subtyping. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 441–457. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_26

    Chapter  MATH  Google Scholar 

  19. Lindley, S., Morris, J.G.: Embedding session types in Haskell. In: Haskell 2016, pp. 133–145 (2016)

    Google Scholar 

  20. Mostrous, D., Yoshida, N.: Session typing and asynchronous subtyping for the higher-order \(\pi \)-calculus. Inf. Comput. 241, 227–263 (2015)

    Article  MathSciNet  Google Scholar 

  21. Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00590-9_23

    Chapter  Google Scholar 

  22. Mota, J., Giunti, M., Ravara, A.: Java typestate checker. In: Damiani, F., Dardha, O. (eds.) COORDINATION 2021. LNCS, vol. 12717, pp. 121–133. Springer, Cham (2021)

    Google Scholar 

  23. Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation for distributed protocols with interaction refinements in F\(\sharp \). In: CC 2018. ACM (2018)

    Google Scholar 

  24. Orchard, D.A., Yoshida, N.: Effects as sessions, sessions as effects. In: Principles of Programming Languages (POPL 2016), pp. 568–581 (2016)

    Google Scholar 

  25. Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, e4 (2017)

    Article  MathSciNet  Google Scholar 

  26. Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: European Conference on Object-Oriented Programming (ECOOP 2016), pp. 21:1–21:28 (2016)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Bologna, Bologna, Italy

    Lorenzo Bacchiani, Mario Bravetti & Gianluigi Zavattaro

  2. Focus Team, Inria, Sophia Antipolis, France

    Mario Bravetti & Gianluigi Zavattaro

  3. Royal Holloway, University of London, Egham, UK

    Julien Lange

Authors
  1. Lorenzo Bacchiani
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mario Bravetti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Julien Lange
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gianluigi Zavattaro
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lorenzo Bacchiani .

Editor information

Editors and Affiliations

  1. University of Turin, Turin, Italy

    Ferruccio Damiani

  2. Sir Alwyn William Building, University of Glasgow, Glasgow, UK

    Ornela Dardha

Rights and permissions

Reprints and permissions

Copyright information

© 2021 IFIP International Federation for Information Processing

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bacchiani, L., Bravetti, M., Lange, J., Zavattaro, G. (2021). A Session Subtyping Tool. In: Damiani, F., Dardha, O. (eds) Coordination Models and Languages. COORDINATION 2021. Lecture Notes in Computer Science(), vol 12717. Springer, Cham. https://doi.org/10.1007/978-3-030-78142-2_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-78142-2_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-78141-5

  • Online ISBN: 978-3-030-78142-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation