<XML><RECORDS><RECORD><REFERENCE_TYPE>10</REFERENCE_TYPE><REFNUM>8588</REFNUM><AUTHORS><AUTHOR>Gay,S.J.</AUTHOR><AUTHOR>Vasconcelos,V.T.</AUTHOR></AUTHORS><YEAR>2007</YEAR><TITLE>Asynchronous Functional Session Types</TITLE><PLACE_PUBLISHED>DCS Technical Report Series</PLACE_PUBLISHED><PUBLISHER>Dept of Computing Science, University of Glasgow</PUBLISHER><ISBN>TR-2007-251</ISBN><LABEL>Gay:2007:8588</LABEL><KEYWORDS><KEYWORD>Session types</KEYWORD></KEYWORDS<ABSTRACT>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 three main contributions. First: an operational semantics with buffered channels, instead of the synchronous communication of previous work. Second: session type manipulation by means of the standard structures of a linear type theory, rather than by means of new forms of typing judgement. Third: a notion of subtyping, including the standard subtyping relation for session types (imported into the functional setting) and a novel form of subtyping between standard and linear function types. Our new approach significantly simplifies session types in the functional setting, clarifies their essential features, and provides a secure foundation for language developments such as polymorphism and object-orientation, as well as further forms of static analysis including estimating the size of communication buffers.</ABSTRACT></RECORD></RECORDS></XML>