Sciweavers

Share
JFP
2010

Linear type theory for asynchronous session types

11 years 5 months ago
Linear type theory for asynchronous session types
Session types support a type-theoretic formulation of structured patterns of communication, so that the communication behaviour of agents in a distributed system can be verified by static type checking. Applications include network protocols, business processes, and operating system services. In this paper we define a multithreaded functional language with session types, which unifies, simplifies and extends previous work. There are four main contributions. First: an operational semantics with buffered channels, instead of the synchronous communication of previous work. Second: we prove that the session type of a channel gives an upper bound on the necessary size of the buffer. Third: session types are manipulated by means of the standard structures of a linear type theory, rather than by means of new forms of typing judgement. Fourth: a notion of subtyping, including the standard subtyping relation for session types (imported into the functional setting), and a novel form of subt...
Simon J. Gay, Vasco Thudichum Vasconcelos
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Where JFP
Authors Simon J. Gay, Vasco Thudichum Vasconcelos
Comments (0)
books