Linear type theory for asynchronous session types

13 years 3 months ago

Download www.dcs.gla.ac.uk

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 veriﬁed by static type checking. Applications include network protocols, business processes, and operating system services. In this paper we deﬁne a multithreaded functional language with session types, which uniﬁes, simpliﬁes 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

Real-time Traffic