%0 Conference Proceedings
%T Relating Functional and Imperative Session Types
%+ University of Freiburg [Freiburg]
%A Saffrich, Hannes
%A Thiemann, Peter
%Z Part 2: Communications: Types and Implemenations
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 23th International Conference on Coordination Languages and Models (COORDINATION)
%C Valletta, Malta
%Y Ferruccio Damiani
%Y Ornela Dardha
%I Springer International Publishing
%3 Coordination Models and Languages
%V LNCS-12717
%P 61-79
%8 2021-06-14
%D 2021
%R 10.1007/978-3-030-78142-2_4
%K Session types
%K Distributed programming
%K Translation
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-03387840/document
%2 https://inria.hal.science/hal-03387840/file/509400_1_En_4_Chapter.pdf
%L hal-03387840
%U https://inria.hal.science/hal-03387840
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-COORDINATION
%~ IFIP-LNCS-12717