Subtyping for session types in the pi calculus

Extending the pi calculus with the session types proposed by Honda et al. allows high-level specifications of structured patterns of communication, such as client-server protocols, to be expressed as types and verified by static typechecking. We define a notion of subtyping for session types, which allows protocol specifications to be extended in order to describe richer behaviour; for example, an implemented server can be refined without invalidating type-correctness of an overall system. We formalize the syntax, operational semantics and typing rules of an extended pi calculus, prove that typability guarantees absence of run-time communication errors, and show that the typing rules can be transformed into a practical typechecking algorithm.

• Type: Journal
• Year: 2005
• Where: ACTA
• Authors: Simon J. Gay, Malcolm Hole
• Keywords: ACTA 2005, Extended Pi Calculus, Session Types, Static Typechecking