A Bounded Polymorphic Session Type System with Delegation

摘要

Two notions of subtyping and bounded polymorphism have been proposed to increase the expressiveness of session types. In this paper, we propose a new bounded polymorphic type system in which we incorporate the two notions and add delegation to the typing rules. As a result, this system not only can support more flexible specification protocols but also can express high-order communications, i.e. channel passing which can change the structure radically. At last, the soundness of this type system is proved by demonstrating Subject Reduction Theorem and Type Safety.