Linear type theory for asynchronous session types
- 8 December 2009
- journal article
- research article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 20 (1), 19-50
- https://doi.org/10.1017/s0956796809990268
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 typechecking. 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 is 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 subtyping between standard and linear function types, which allows the typechecker to handle linear types conveniently. 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.Keywords
This publication has 20 references indexed in Scilit:
- Amalgamating sessions and methods in object-oriented languages with genericsTheoretical Computer Science, 2009
- Bounded polymorphism in session typesMathematical Structures in Computer Science, 2008
- Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session CommunicationElectronic Notes in Theoretical Computer Science, 2007
- Type checking a multithreaded functional language with session typesTheoretical Computer Science, 2006
- Subtyping for session types in the pi calculusActa Informatica, 2005
- Correspondence assertions for process synchronization in concurrent communicationsJournal of Functional Programming, 2005
- An Implementation of Session TypesLecture Notes in Computer Science, 2004
- Protocol SpecializationLecture Notes in Computer Science, 2004
- Language primitives and type discipline for structured communication-based programmingPublished by Springer Science and Business Media LLC ,1998
- A Syntactic Approach to Type SoundnessInformation and Computation, 1994