Bounded polymorphism in session types
- 1 February 2008
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 18 (5), 895-930
- https://doi.org/10.1017/s0960129508006944
Abstract
Session types allow high-level specifications of structured patterns of communication, such as client-server protocols, to be expressed as types and verified by static typechecking. In collaboration with Malcolm Hole, we previously introduced a notion of subtyping for session types, which was formulated for an extended pi calculus. Subtyping allows one part of a system, for example, a server, to be refined without invalidating type-correctness of other parts, for example, clients. In this paper we introduce bounded polymorphism, which is based on the same notion of subtyping, in order to support more precise and flexible specifications of protocols; in particular, a choice of type in one message may affect the types of future messages. We formalise the syntax, operational semantics and typing rules of an extended pi calculus, and prove that typechecking guarantees the absence of run-time communication errors. We study algorithms for checking instances of the subtype relation in two versions of our system, which we call KernelS≤and FullS≤, and establish that subtyping in KernelS≤is decidable, and that subtyping in FullS≤is undecidable.Keywords
This publication has 21 references indexed in Scilit:
- 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
- Session Types for Functional MultithreadingLecture Notes in Computer Science, 2004
- Behavioral equivalence in the polymorphic pi-calculusJournal of the ACM, 2000
- Linearity and the pi-calculusACM Transactions on Programming Languages and Systems, 1999
- Language primitives and type discipline for structured communication-based programmingPublished by Springer Science and Business Media LLC ,1998
- A calculus of mobile processes, IInformation and Computation, 1992
- Linear logicTheoretical Computer Science, 1987
- On understanding types, data abstraction, and polymorphismACM Computing Surveys, 1985