A Polymorphic Type System with Progress for Binary Sessions

摘要

A static bounded polymorphic type system is presented in this paper, which ensures the progress property, i.e., the property that once a communication has been established, well-formed programs will never starve at communication points. The introduction of subtyping for session types and the relaxed duality relation increases the flexibility of the type system, and allows the participants in a conversation to follow different protocols that are nevertheless compatible in a sense defined by the subtyping relation. In addition, to keep progress in sessions, the type compliance is defined to associate with the relaxed duality relation, where the environment is balanced. Finally, the soundness and communication safety of the type system are proved, and some related work and possible future work in this area are discussed.