An Extensible Approach to Session Polymorphism

Existing session typing systems have limited support for polymorphic typing. For example, existing systems cannot provide the most general type for a generic proxy process that forwards messages between two channels. We define a session typing system for processes which can assign such a type. The type system is parameterized by a metatheory in which session constructors are defined, allowing easy creation of new session constructors. In this paper, we express the metatheory in Coq's specification language. The proof of subject reduction and typing of examples have been mechanically verified with the Coq theorem prover.