Mostrous, Dimitris and Vasconcelos, Vasco T. - Affine Sessions

lmcs:4815 - Logical Methods in Computer Science, November 15, 2018, Volume 14, Issue 4
Affine Sessions

Authors: Mostrous, Dimitris and Vasconcelos, Vasco T.

Session types describe the structure of communications implemented by channels. In particular, they prescribe the sequence of communications, whether they are input or output actions, and the type of value exchanged. Crucial to any language with session types is the notion of linearity, which is essential to ensure that channels exhibit the behaviour prescribed by their type without interference in the presence of concurrency. In this work we relax the condition of linearity to that of affinity, by which channels exhibit at most the behaviour prescribed by their types. This more liberal setting allows us to incorporate an elegant error handling mechanism which simplifies and improves related works on exceptions. Moreover, our treatment does not affect the progress properties of the language: sessions never get stuck.


Source : oai:arXiv.org:1809.02781
DOI : 10.23638/LMCS-14(4:14)2018
Volume: Volume 14, Issue 4
Published on: November 15, 2018
Submitted on: September 11, 2018
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.3.2,F.4.1


Share