Skip to main content
SpringerLink
Log in

Relating Functional and Imperative Session Types

  • 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:

  • 596 Accesses

Abstract

Imperative session types provide an imperative interface to session-typed communication in a functional language. Compared to functional session type APIs, the program structure is simpler at the surface, but typestate is required to model the current state of communication throughout.

Most work on session types has neglected the imperative approach. We demonstrate that the functional approach subsumes previous work on imperative session types by exhibiting a typing and semantics preserving translation into a system of linear functional session types.

We further show that the untyped backwards translation from the functional to the imperative calculus is semantics preserving. We restrict the type system of the functional calculus such that the backwards translation becomes type preserving. Thus, we precisely capture the difference in expressiveness of the two calculi and conclude that the lack of expressiveness in the imperative calculus is solely due to its type system.

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.

    The conference version of their paper [28] is called “Session Types for Functional Multithreading”.

  2. 2.

    Uppercase letters denote types in the VGR calculus.

  3. 3.

    Linear Functional Session Types.

  4. 4.

    \(\textsf {let}\,x=\textsf {fork}\,t; t'\,\textsf {in}\, t''\) is stuck in the original work [27].

References

  1. Allais, G.: Typing with leftovers - a mechanization of intuitionistic multiplicative-additive linear logic. In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017. LIPIcs, Budapest, Hungary, May 29–June 1, 2017, vol. 104, pp. 1:1–1:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017). https://doi.org/10.4230/LIPIcs.TYPES.2017.1

  2. Atkey, R.: Parameterised notions of computation. J. Funct. Program. 19(3–4), 335–376 (2009). https://doi.org/10.1017/S095679680900728X

    Article  MathSciNet  MATH  Google Scholar 

  3. Balzer, S., Toninho, B., Pfenning, F.: Manifest Deadlock-freedom for shared session types. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 611–639. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17184-1_22

    Chapter  Google Scholar 

  4. 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_16

    Chapter  Google Scholar 

  5. Das, A., Pfenning, F.: Session types with arithmetic refinements. In: Konnov, I., Kovács, L. (eds.) 31st International Conference on Concurrency Theory, CONCUR 2020 (Virtual Conference). LIPIcs, Vienna, Austria, 1–4 September 2020, vol. 171, pp. 13:1–13:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPIcs.CONCUR.2020.13

  6. Fowler, S., Lindley, S., Morris, J.G., Decova, S.: Exceptional asynchronous session types: session types without tiers. Proc. ACM Program. Lang. 3(POPL), 28:1–28:29 (2019). https://doi.org/10.1145/3290341

  7. Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19–50 (2010). https://doi.org/10.1017/S0956796809990268

    Article  MathSciNet  MATH  Google Scholar 

  8. Gordon, C.S.: A generic approach to flow-sensitive polymorphic effects. In: 31st European Conference on Object-Oriented Programming, ECOOP 2017. LIPIcs, Barcelona, Spain, 19–23 June 2017, vol. 74, pp. 13:1–13:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017). https://doi.org/10.4230/LIPIcs.ECOOP.2017.13

  9. Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57208-2_35

    Chapter  Google Scholar 

  10. Hu, R., Kouzapas, D., Pernet, O., Yoshida, N., Honda, K.: Type-safe eventful sessions in Java. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 329–353. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14107-2_16

    Chapter  Google Scholar 

  11. 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 

  12. Imai, K., Yoshida, N., Yuen, S.: Session-OCaml: a session-based library with polarities and lenses. Sci. Comput. Program. 172, 135–159 (2019). https://doi.org/10.1016/j.scico.2018.08.005

    Article  Google Scholar 

  13. Milner, R.: Communicating and Mobile Systems - The Pi-Calculus. Cambridge University Press, New York (1999)

    MATH  Google Scholar 

  14. Padovani, L.: Context-free session type inference. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 804–830. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54434-1_30

    Chapter  Google Scholar 

  15. Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, e4 (2017). https://doi.org/10.1017/S0956796816000289

    Article  MathSciNet  MATH  Google Scholar 

  16. Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975). https://doi.org/10.1016/0304-3975(75)90017-1

    Article  MATH  Google Scholar 

  17. Pucella, R., Tov, J.A.: Haskell session types with (almost) no class. In: Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, Haskell 2008, Victoria, BC, Canada, 25 September 2008, pp. 25–36. ACM (2008). https://doi.org/10.1145/1411286.1411290

  18. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, 22–25 July 2002, Proceedings, pp. 55–74. IEEE Computer Society (2002). https://doi.org/10.1109/LICS.2002.1029817

  19. Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. LISP Symb. Comput. 6(3–4), 289–360 (1993)

    Google Scholar 

  20. Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Trans. Program. Lang. Syst. 19(6), 916–941 (1997). https://doi.org/10.1145/267959.269968

    Article  MATH  Google Scholar 

  21. Sackman, M., Eisenbach, S.: Session types in Haskell updating message passing for the 21st century (2008). https://spiral.imperial.ac.uk:8443/handle/10044/1/5918

  22. Scalas, A., Yoshida, N.: Lightweight session programming in Scala. In: 30th European Conference on Object-Oriented Programming, ECOOP 2016. LIPIcs, Rome, Italy, 18–22 July 2016, vol. 56, pp. 21:1–21:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016). https://doi.org/10.4230/LIPIcs.ECOOP.2016.21

  23. Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 366–381. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46425-5_24

    Chapter  Google Scholar 

  24. Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Software Eng. 12(1), 157–171 (1986). https://doi.org/10.1109/TSE.1986.6312929

    Article  MATH  Google Scholar 

  25. Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58184-7_118

    Chapter  Google Scholar 

  26. Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: a monadic integration. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 350–369. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_20

    Chapter  MATH  Google Scholar 

  27. Vasconcelos, V.T., Gay, S.J., Ravara, A.: Type checking a multithreaded functional language with session types. Theor. Comput. Sci. 368(1–2), 64–87 (2006). https://doi.org/10.1016/j.tcs.2006.06.028

    Article  MathSciNet  MATH  Google Scholar 

  28. Vasconcelos, V., Ravara, A., Gay, S.: Session types for functional multithreading. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 497–511. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_32

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Freiburg, Freiburg im Breisgau, Germany

    Hannes Saffrich & Peter Thiemann

Authors
  1. Hannes Saffrich
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Thiemann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Thiemann .

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

Saffrich, H., Thiemann, P. (2021). Relating Functional and Imperative Session Types. 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_4

Download citation

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

  • 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