Skip to Main content Skip to Navigation
New interface
Conference papers

Relating Functional and Imperative Session Types

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.
Complete list of metadata
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, October 20, 2021 - 9:01:22 AM
Last modification on : Wednesday, October 20, 2021 - 10:21:24 AM
Long-term archiving on: : Friday, January 21, 2022 - 7:18:15 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2024-01-01

Please log in to resquest access to the document


Distributed under a Creative Commons Attribution 4.0 International License



Hannes Saffrich, Peter Thiemann. Relating Functional and Imperative Session Types. 23th International Conference on Coordination Languages and Models (COORDINATION), Jun 2021, Valletta, Malta. pp.61-79, ⟨10.1007/978-3-030-78142-2_4⟩. ⟨hal-03387840⟩



Record views