Asynchronous sessions with implicit functions and messages

Jeffery, Alexander and Berger, Martin (2018) Asynchronous sessions with implicit functions and messages. 12th International Symposium on Theoretical Aspects of Software Engineering, Guangzhou, China, August 29-31 2018. Published in: 2018 International Symposium on Theoretical Aspects of Software Engineering (TASE). Institute of Electrical and Electronics Engineers ISBN 9781538673058

[img] PDF (©IEEE) - Accepted Version
Available under License All Rights Reserved.

Download (357kB)

Abstract

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 presenting the first concurrent functional language with implicit message passing. The key idea is to generalise the concept of an implicit function to an implicit message, its concurrent analogue. Our language extends Gay and Vasconcelos’s calculus of linear types for asynchronous sessions (LAST) with implicit functions and messages. We prove the resulting system sound by translation into LAST.

Item Type: Conference Proceedings
Schools and Departments: School of Engineering and Informatics > Informatics
Research Centres and Groups: Foundations of Software Systems
Related URLs:
Depositing User: Martin Berger
Date Deposited: 26 Jul 2018 09:22
Last Modified: 18 Jan 2019 15:45
URI: http://sro.sussex.ac.uk/id/eprint/77383

View download statistics for this item

📧 Request an update