Computing at Glasgow University
Paper ID: 8588
DCS Tech Report Number: TR-2007-251

Asynchronous Functional Session Types
Gay,S.J. Vasconcelos,V.T.

Publication Type: Tech Report (internal)
Appeared in: DCS Technical Report Series
Page Numbers :
Publisher: Dept of Computing Science, University of Glasgow
Year: 2007

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.

Keywords: Session types, functional programming, typechecking, semantics, distributed programming, specification of communication protocol

PDF Bibtex entry Endnote XML