Relating Functional and Imperative Session Types - Coordination Models and Languages Access content directly
Conference Papers Year : 2021

Relating Functional and Imperative Session Types

Hannes Saffrich
  • Function : Author
  • PersonId : 1114101
Peter Thiemann
  • Function : Author
  • PersonId : 1114103


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.
Fichier principal
Vignette du fichier
509400_1_En_4_Chapter.pdf (438.86 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03387840 , version 1 (20-10-2021)





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⟩
23 View
13 Download



Gmail Facebook X LinkedIn More