Asynchronous sessions with implicit functions and messages

Jeffery, Alex and Berger, Martin (2020) Asynchronous sessions with implicit functions and messages. Science of Computer Programming. ISSN 0167-6423

[img] PDF - Accepted Version
Available under License Creative Commons Attribution-NonCommercial No Derivatives.

Download (734kB)


Session types are a well-established approach to ensuring protocol conformance and the absence of communication errors such as deadlocks in message passing systems. Haskell introduced implicit parameters, Scala popularised this feature and recently gave implicit types first-class status, yielding an expressive tool for handling context dependencies in a type-safe yet terse way. We ask: can type-safe implicit functions be generalised from Scala's sequential setting to message passing computation? We answer this question in the affirmative by generalising the concept of an implicit function to an implicit message, its concurrent analogue. We present two calculi, each with implicit message passing. The first, Im, is a concurrent functional language that extends Gay and Vasconcelos's calculus of linear types for asynchronous sessions (Last) with implicit functions and messages. The second, MpIm, is a π-calculus with implicit messages that extends Coppo, Dezani-Ciancaglini, Padovani and Yoshida's calculus of multiparty asynchronous sessions (Mpst ). We argue, via examples, that these new language features provide utility to the programmer, and prove each system sound by translation into its respective base calculus.

Item Type: Article
Schools and Departments: School of Engineering and Informatics > Informatics
Research Centres and Groups: Foundations of Software Systems
Depositing User: Martin Berger
Date Deposited: 11 Apr 2019 10:31
Last Modified: 18 May 2020 01:00

View download statistics for this item

📧 Request an update