An extensible approach to session polymorphism

摘要

Session types describe and constrain the input/output behaviour of systems. Existing sessionrntyping systems have limited support for polymorphism. For example, existing systemsrncannot provide the most general type for a generic proxy process that forwards messagesrnbetween two channels. We provide a polymorphic session typing system for the π calculus,rnand demonstrate the utility of session-type-level functions in combination with polymorphicrnsession typing. The type system guarantees subject reduction and safety properties, but notrndeadlock freedom. We describe a formalization of the type system in Coq. The proofs ofrnsubject reduction and safety properties, as well as typing of example processes, have beenrnmechanically verified.